This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )