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 e. _V
	ab2rexex2.2	|- B e. _V
	ab2rexex2.3	|- { z | ph } e. _V
Assertion	ab2rexex2	|- { z | E. x e. A E. y e. B ph } e. _V

Proof

Step	Hyp	Ref	Expression
1		ab2rexex2.1	|- A e. _V
2		ab2rexex2.2	|- B e. _V
3		ab2rexex2.3	|- { z | ph } e. _V
4	2 3	abrexex2	|- { z | E. y e. B ph } e. _V
5	1 4	abrexex2	|- { z | E. x e. A E. y e. B ph } e. _V