Theorem rexiunxp

Description: Write a double restricted quantification as one universal quantifier. In this version of rexxp , B ( y ) is not assumed to be constant. (Contributed by Mario Carneiro, 14-Feb-2015)

	Ref	Expression
Hypothesis	ralxp.1	|- ( x = <. y , z >. -> ( ph <-> ps ) )
Assertion	rexiunxp	|- ( E. x e. U_ y e. A ( { y } 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	1	notbid	|- ( x = <. y , z >. -> ( -. ph <-> -. ps ) )
3	2	raliunxp	|- ( A. x e. U_ y e. A ( { y } X. B ) -. ph <-> A. y e. A A. z e. B -. ps )
4		ralnex	|- ( A. z e. B -. ps <-> -. E. z e. B ps )
5	4	ralbii	|- ( A. y e. A A. z e. B -. ps <-> A. y e. A -. E. z e. B ps )
6	3 5	bitri	|- ( A. x e. U_ y e. A ( { y } X. B ) -. ph <-> A. y e. A -. E. z e. B ps )
7	6	notbii	|- ( -. A. x e. U_ y e. A ( { y } X. B ) -. ph <-> -. A. y e. A -. E. z e. B ps )
8		dfrex2	|- ( E. x e. U_ y e. A ( { y } X. B ) ph <-> -. A. x e. U_ y e. A ( { y } X. B ) -. ph )
9		dfrex2	|- ( E. y e. A E. z e. B ps <-> -. A. y e. A -. E. z e. B ps )
10	7 8 9	3bitr4i	|- ( E. x e. U_ y e. A ( { y } X. B ) ph <-> E. y e. A E. z e. B ps )