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

Metamath Proof Explorer

Theorem ralrn

Description: Restricted universal quantification over the range of a function. (Contributed by Mario Carneiro, 24-Dec-2013) (Revised by Mario Carneiro, 20-Aug-2014)

Ref Expression
Hypothesis rexrn.1 
|- ( x = ( F ` y ) -> ( ph <-> ps ) )
Assertion ralrn 
|- ( F Fn A -> ( A. x e. ran F ph <-> A. y e. A ps ) )

Proof

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