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	$$⊢A\in \mathrm{V}$$
	ab2rexex.2	$$⊢B\in \mathrm{V}$$
Assertion	ab2rexex	$$⊢\left\{z|\exists x\in A\exists y\in Bz=C\right\}\in \mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		ab2rexex.1	$$⊢A\in \mathrm{V}$$
2		ab2rexex.2	$$⊢B\in \mathrm{V}$$
3	2	abrexex	$$⊢\left\{z|\exists y\in Bz=C\right\}\in \mathrm{V}$$
4	1 3	abrexex2	$$⊢\left\{z|\exists x\in A\exists y\in Bz=C\right\}\in \mathrm{V}$$