 Forcing theorem

The forcing theorem identifies truth in a generic extension with the forcing relation: a formula is true in $M[G]$ exactly when some condition in $G$ forces it.