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	\|- 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