The Truth Lemma
The result says that what's true in a forcing extension $M[G]$ is just what's forced to be true by the path of the generic filter $G$. More precisely:
Suppose $M$ is a countable transitive model of $\text{ZFC}$, $\mathbb{P} \in M$ a forcing poset, $\varphi(x_1, \dots, x_n)$ a set theoretical formula, and $\tau_1, \dots, \tau_n$ a sequence of $\mathbb{P}$-names in $M$. If a filter $G$ on $\mathbb{P}$ meets each dense subset of $\mathbb{P}$ in $M$, then $\varphi(\tau_1^G, \dots, \tau_n^G)$ holds in $M[G]$ iff $G$ hits a $p$ that forces $\varphi(\tau_1, \dots, \tau_n)$.
In fact, $M$ just needs to satisfy a rich enough finite subtheory of $\text{ZFC}$. (How rich depends on $\varphi$.) Therefore the existence of suitable $M$ follows from the Reflection Theorem, which can be proved in $\text{ZFC}$ without assuming that $\text{ZFC}$ has a countable transitive model.
With a result known as the Definability Lemma, the Truth Lemma implies that every partial order forces $\text{ZFC}$. That is, $\text{ZFC}$ holds in every $M[G]$—no matter the $M$, $\mathbb{P}$, or $G$. This is key to showing that $M[G]$ is always the smallest transitive extension of $M$ satisfying $\text{ZFC}$ and containing $G$ as an element. Thus, in diverse circumstances one may build the partial order $\mathbb{P}$ of attempts to construct a desired object, argue that the object exists in any extension of $M$ containing a filter $G$ as in the lemma, and thereby obtain the actual existence of the desired object in a model where the axioms of ZFC still hold. Magic!
