Theorem ab2rexex2

Description: Existence of an existentially restricted class abstraction. ph normally has free-variable parameters x , y , and z . Compare abrexex2 . (Contributed by NM, 20-Sep-2011)

	Ref	Expression
Hypotheses	ab2rexex2.1	⊢ 𝐴 ∈ V
	ab2rexex2.2	⊢ 𝐵 ∈ V
	ab2rexex2.3	⊢ { 𝑧 ∣ 𝜑 } ∈ V
Assertion	ab2rexex2	⊢ { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 } ∈ V

Proof

Step	Hyp	Ref	Expression
1		ab2rexex2.1	⊢ 𝐴 ∈ V
2		ab2rexex2.2	⊢ 𝐵 ∈ V
3		ab2rexex2.3	⊢ { 𝑧 ∣ 𝜑 } ∈ V
4	2 3	abrexex2	⊢ { 𝑧 ∣ ∃ 𝑦 ∈ 𝐵 𝜑 } ∈ V
5	1 4	abrexex2	⊢ { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝜑 } ∈ V