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	$$⊢A\in \mathrm{V}$$
	ab2rexex2.2	$$⊢B\in \mathrm{V}$$
	ab2rexex2.3	$$⊢\left\{z|\phi \right\}\in \mathrm{V}$$
Assertion	ab2rexex2	$$⊢\left\{z|\exists x\in A\exists y\in B\phi \right\}\in \mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		ab2rexex2.1	$$⊢A\in \mathrm{V}$$
2		ab2rexex2.2	$$⊢B\in \mathrm{V}$$
3		ab2rexex2.3	$$⊢\left\{z|\phi \right\}\in \mathrm{V}$$
4	2 3	abrexex2	$$⊢\left\{z|\exists y\in B\phi \right\}\in \mathrm{V}$$
5	1 4	abrexex2	$$⊢\left\{z|\exists x\in A\exists y\in B\phi \right\}\in \mathrm{V}$$