Metamath Proof Explorer


Theorem rexxfr

Description: Transfer existence from a variable x to another variable y contained in expression A . (Contributed by NM, 10-Jun-2005) (Revised by Mario Carneiro, 15-Aug-2014)

Ref Expression
Hypotheses ralxfr.1
|- ( y e. C -> A e. B )
ralxfr.2
|- ( x e. B -> E. y e. C x = A )
ralxfr.3
|- ( x = A -> ( ph <-> ps ) )
Assertion rexxfr
|- ( E. x e. B ph <-> E. y e. C ps )

Proof

Step Hyp Ref Expression
1 ralxfr.1
 |-  ( y e. C -> A e. B )
2 ralxfr.2
 |-  ( x e. B -> E. y e. C x = A )
3 ralxfr.3
 |-  ( x = A -> ( ph <-> ps ) )
4 dfrex2
 |-  ( E. x e. B ph <-> -. A. x e. B -. ph )
5 dfrex2
 |-  ( E. y e. C ps <-> -. A. y e. C -. ps )
6 3 notbid
 |-  ( x = A -> ( -. ph <-> -. ps ) )
7 1 2 6 ralxfr
 |-  ( A. x e. B -. ph <-> A. y e. C -. ps )
8 5 7 xchbinxr
 |-  ( E. y e. C ps <-> -. A. x e. B -. ph )
9 4 8 bitr4i
 |-  ( E. x e. B ph <-> E. y e. C ps )