Metamath Proof Explorer


Theorem rexrn

Description: Restricted existential 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 rexrn
|- ( F Fn A -> ( E. x e. ran F ph <-> E. 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 rexxfr2d
 |-  ( F Fn A -> ( E. x e. ran F ph <-> E. y e. A ps ) )