This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ab2rexex

Description: Existence of a class abstraction of existentially restricted sets. Variables x and y are normally free-variable parameters in the class expression substituted for C , which can be thought of as C ( x , y ) . See comments for abrexex . (Contributed by NM, 20-Sep-2011)

	Ref	Expression
Hypotheses	ab2rexex.1	⊢ 𝐴 ∈ V
	ab2rexex.2	⊢ 𝐵 ∈ V
Assertion	ab2rexex	⊢ { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑧 = 𝐶 } ∈ V

Proof

Step	Hyp	Ref	Expression
1		ab2rexex.1	⊢ 𝐴 ∈ V
2		ab2rexex.2	⊢ 𝐵 ∈ V
3	2	abrexex	⊢ { 𝑧 ∣ ∃ 𝑦 ∈ 𝐵 𝑧 = 𝐶 } ∈ V
4	1 3	abrexex2	⊢ { 𝑧 ∣ ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐵 𝑧 = 𝐶 } ∈ V