Metamath Proof Explorer


Theorem elrnmpt

Description: The range of a function in maps-to notation. (Contributed by Mario Carneiro, 20-Feb-2015)

Ref Expression
Hypothesis rnmpt.1
|- F = ( x e. A |-> B )
Assertion elrnmpt
|- ( C 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 eqeq1
 |-  ( y = C -> ( y = B <-> C = B ) )
3 2 rexbidv
 |-  ( y = C -> ( E. x e. A y = B <-> E. x e. A C = B ) )
4 1 rnmpt
 |-  ran F = { y | E. x e. A y = B }
5 3 4 elab2g
 |-  ( C e. V -> ( C e. ran F <-> E. x e. A C = B ) )