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

Metamath Proof Explorer

Theorem ralxfrALT

Description: Alternate proof of ralxfr which does not use ralxfrd . (Contributed by NM, 10-Jun-2005) (Revised by Mario Carneiro, 15-Aug-2014) (Proof modification is discouraged.) (New usage is discouraged.)

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 ralxfrALT 
|- ( A. x e. B ph <-> A. 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 3 rspcv 
 |-  ( A e. B -> ( A. x e. B ph -> ps ) )
5 1 4 syl 
 |-  ( y e. C -> ( A. x e. B ph -> ps ) )
6 5 com12 
 |-  ( A. x e. B ph -> ( y e. C -> ps ) )
7 6 ralrimiv 
 |-  ( A. x e. B ph -> A. y e. C ps )
8 nfra1 
 |-  F/ y A. y e. C ps
9 nfv 
 |-  F/ y ph
10 rsp 
 |-  ( A. y e. C ps -> ( y e. C -> ps ) )
11 3 biimprcd 
 |-  ( ps -> ( x = A -> ph ) )
12 10 11 syl6 
 |-  ( A. y e. C ps -> ( y e. C -> ( x = A -> ph ) ) )
13 8 9 12 rexlimd 
 |-  ( A. y e. C ps -> ( E. y e. C x = A -> ph ) )
14 2 13 syl5 
 |-  ( A. y e. C ps -> ( x e. B -> ph ) )
15 14 ralrimiv 
 |-  ( A. y e. C ps -> A. x e. B ph )
16 7 15 impbii 
 |-  ( A. x e. B ph <-> A. y e. C ps )