Theorem rexxp

Description: Existential quantification restricted to a Cartesian product is equivalent to a double restricted quantification. (Contributed by NM, 11-Nov-1995) (Revised by Mario Carneiro, 14-Feb-2015)

	Ref	Expression
Hypothesis	ralxp.1	|- ( x = <. y , z >. -> ( ph <-> ps ) )
Assertion	rexxp	|- ( E. x e. ( A X. B ) ph <-> E. y e. A E. z e. B ps )

Proof

Step	Hyp	Ref	Expression
1		ralxp.1	|- ( x = <. y , z >. -> ( ph <-> ps ) )
2		iunxpconst	|- U_ y e. A ( { y } X. B ) = ( A X. B )
3	2	rexeqi	|- ( E. x e. U_ y e. A ( { y } X. B ) ph <-> E. x e. ( A X. B ) ph )
4	1	rexiunxp	|- ( E. x e. U_ y e. A ( { y } X. B ) ph <-> E. y e. A E. z e. B ps )
5	3 4	bitr3i	|- ( E. x e. ( A X. B ) ph <-> E. y e. A E. z e. B ps )