Forcing definability lemma
= Forcing definability lemma
For each formula, its forcing relation on names and conditions is uniformly first-order definable inside the ground model. This permits ground-model separation and replacement using forcing predicates.