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

Metamath Proof Explorer

Theorem elrnmptg

Description: Membership in the range of a function. (Contributed by NM, 27-Aug-2007) (Revised by Mario Carneiro, 31-Aug-2015)

Ref Expression
Hypothesis rnmpt.1 
|- F = ( x e. A |-> B )
Assertion elrnmptg 
|- ( A. x e. A B e. V -> ( C e. ran F <-> E. x e. A C = B ) )

Proof

Step Hyp Ref Expression
1 rnmpt.1 
 |-  F = ( x e. A |-> B )
2 1 rnmpt 
 |-  ran F = { y | E. x e. A y = B }
3 2 eleq2i 
 |-  ( C e. ran F <-> C e. { y | E. x e. A y = B } )
4 r19.29 
 |-  ( ( A. x e. A B e. V /\ E. x e. A C = B ) -> E. x e. A ( B e. V /\ C = B ) )
5 eleq1 
 |-  ( C = B -> ( C e. V <-> B e. V ) )
6 5 biimparc 
 |-  ( ( B e. V /\ C = B ) -> C e. V )
7 6 elexd 
 |-  ( ( B e. V /\ C = B ) -> C e. _V )
8 7 rexlimivw 
 |-  ( E. x e. A ( B e. V /\ C = B ) -> C e. _V )
9 4 8 syl 
 |-  ( ( A. x e. A B e. V /\ E. x e. A C = B ) -> C e. _V )
10 9 ex 
 |-  ( A. x e. A B e. V -> ( E. x e. A C = B -> C e. _V ) )
11 eqeq1 
 |-  ( y = C -> ( y = B <-> C = B ) )
12 11 rexbidv 
 |-  ( y = C -> ( E. x e. A y = B <-> E. x e. A C = B ) )
13 12 elab3g 
 |-  ( ( E. x e. A C = B -> C e. _V ) -> ( C e. { y | E. x e. A y = B } <-> E. x e. A C = B ) )
14 10 13 syl 
 |-  ( A. x e. A B e. V -> ( C e. { y | E. x e. A y = B } <-> E. x e. A C = B ) )
15 3 14 bitrid 
 |-  ( A. x e. A B e. V -> ( C e. ran F <-> E. x e. A C = B ) )