Metamath Proof Explorer


Theorem elrnmptd

Description: The range of a function in maps-to notation. (Contributed by Glauco Siliprandi, 17-Aug-2020)

Ref Expression
Hypotheses elrnmptd.f
|- F = ( x e. A |-> B )
elrnmptd.x
|- ( ph -> E. x e. A C = B )
elrnmptd.c
|- ( ph -> C e. V )
Assertion elrnmptd
|- ( ph -> C e. ran F )

Proof

Step Hyp Ref Expression
1 elrnmptd.f
 |-  F = ( x e. A |-> B )
2 elrnmptd.x
 |-  ( ph -> E. x e. A C = B )
3 elrnmptd.c
 |-  ( ph -> C e. V )
4 1 elrnmpt
 |-  ( C e. V -> ( C e. ran F <-> E. x e. A C = B ) )
5 3 4 syl
 |-  ( ph -> ( C e. ran F <-> E. x e. A C = B ) )
6 2 5 mpbird
 |-  ( ph -> C e. ran F )