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

Metamath Proof Explorer

Theorem rexxpf

Description: Version of rexxp with bound-variable hypotheses. (Contributed by NM, 19-Dec-2008) (Revised by Mario Carneiro, 15-Oct-2016)

Ref Expression
Hypotheses ralxpf.1 
|- F/ y ph
ralxpf.2 
|- F/ z ph
ralxpf.3 
|- F/ x ps
ralxpf.4 
|- ( x = <. y , z >. -> ( ph <-> ps ) )
Assertion rexxpf 
|- ( E. x e. ( A X. B ) ph <-> E. y e. A E. z e. B ps )

Proof

Step Hyp Ref Expression
1 ralxpf.1 
 |-  F/ y ph
2 ralxpf.2 
 |-  F/ z ph
3 ralxpf.3 
 |-  F/ x ps
4 ralxpf.4 
 |-  ( x = <. y , z >. -> ( ph <-> ps ) )
5 1 nfn 
 |-  F/ y -. ph
6 2 nfn 
 |-  F/ z -. ph
7 3 nfn 
 |-  F/ x -. ps
8 4 notbid 
 |-  ( x = <. y , z >. -> ( -. ph <-> -. ps ) )
9 5 6 7 8 ralxpf 
 |-  ( A. x e. ( A X. B ) -. ph <-> A. y e. A A. z e. B -. ps )
10 ralnex 
 |-  ( A. z e. B -. ps <-> -. E. z e. B ps )
11 10 ralbii 
 |-  ( A. y e. A A. z e. B -. ps <-> A. y e. A -. E. z e. B ps )
12 9 11 bitri 
 |-  ( A. x e. ( A X. B ) -. ph <-> A. y e. A -. E. z e. B ps )
13 12 notbii 
 |-  ( -. A. x e. ( A X. B ) -. ph <-> -. A. y e. A -. E. z e. B ps )
14 dfrex2 
 |-  ( E. x e. ( A X. B ) ph <-> -. A. x e. ( A X. B ) -. ph )
15 dfrex2 
 |-  ( E. y e. A E. z e. B ps <-> -. A. y e. A -. E. z e. B ps )
16 13 14 15 3bitr4i 
 |-  ( E. x e. ( A X. B ) ph <-> E. y e. A E. z e. B ps )