Theorem rexabso

Description: Simplification of restricted quantification in a transitive class. When ph is quantifier-free, this shows that the formula E. x e. y ph is absolute for transitive models, which is a particular case of Lemma I.16.2 of Kunen2 p. 95. (Contributed by Eric Schmidt, 19-Oct-2025)

	Ref	Expression
Assertion	rexabso	⊢ ( ( Tr 𝑀 ∧ 𝐴 ∈ 𝑀 ) → ( ∃ 𝑥 ∈ 𝐴 𝜑 ↔ ∃ 𝑥 ∈ 𝑀 ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ) )

Proof

Step	Hyp	Ref	Expression
1		trss	⊢ ( Tr 𝑀 → ( 𝐴 ∈ 𝑀 → 𝐴 ⊆ 𝑀 ) )
2	1	imp	⊢ ( ( Tr 𝑀 ∧ 𝐴 ∈ 𝑀 ) → 𝐴 ⊆ 𝑀 )
3		rexss	⊢ ( 𝐴 ⊆ 𝑀 → ( ∃ 𝑥 ∈ 𝐴 𝜑 ↔ ∃ 𝑥 ∈ 𝑀 ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ) )
4	2 3	syl	⊢ ( ( Tr 𝑀 ∧ 𝐴 ∈ 𝑀 ) → ( ∃ 𝑥 ∈ 𝐴 𝜑 ↔ ∃ 𝑥 ∈ 𝑀 ( 𝑥 ∈ 𝐴 ∧ 𝜑 ) ) )