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

Metamath Proof Explorer

Theorem ralimaOLD

Description: Obsolete version of ralima as of 14-Aug-2025. (Contributed by Stefan O'Rear, 21-Jan-2015) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypothesis reximaOLD.x 
|- ( x = ( F ` y ) -> ( ph <-> ps ) )
Assertion ralimaOLD 
|- ( ( F Fn A /\ B C_ A ) -> ( A. x e. ( F " B ) ph <-> A. y e. B ps ) )

Proof

Step Hyp Ref Expression
1 reximaOLD.x 
 |-  ( x = ( F ` y ) -> ( ph <-> ps ) )
2 fvexd 
 |-  ( ( ( F Fn A /\ B C_ A ) /\ y e. B ) -> ( F ` y ) e. _V )
3 fvelimab 
 |-  ( ( F Fn A /\ B C_ A ) -> ( x e. ( F " B ) <-> E. y e. B ( F ` y ) = x ) )
4 eqcom 
 |-  ( ( F ` y ) = x <-> x = ( F ` y ) )
5 4 rexbii 
 |-  ( E. y e. B ( F ` y ) = x <-> E. y e. B x = ( F ` y ) )
6 3 5 bitrdi 
 |-  ( ( F Fn A /\ B C_ A ) -> ( x e. ( F " B ) <-> E. y e. B x = ( F ` y ) ) )
7 1 adantl 
 |-  ( ( ( F Fn A /\ B C_ A ) /\ x = ( F ` y ) ) -> ( ph <-> ps ) )
8 2 6 7 ralxfr2d 
 |-  ( ( F Fn A /\ B C_ A ) -> ( A. x e. ( F " B ) ph <-> A. y e. B ps ) )