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 e. _V
	ab2rexex.2	|- B e. _V
Assertion	ab2rexex	|- { z | E. x e. A E. y e. B z = C } e. _V

Proof

Step	Hyp	Ref	Expression
1		ab2rexex.1	|- A e. _V
2		ab2rexex.2	|- B e. _V
3	2	abrexex	|- { z | E. y e. B z = C } e. _V
4	1 3	abrexex2	|- { z | E. x e. A E. y e. B z = C } e. _V