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 A B
elrnmptd.x φ x A C = B
elrnmptd.c φ C V
Assertion elrnmptd φ C ran F

Proof

Step Hyp Ref Expression
1 elrnmptd.f F = x A B
2 elrnmptd.x φ x A C = B
3 elrnmptd.c φ C V
4 1 elrnmpt C V C ran F x A C = B
5 3 4 syl φ C ran F x A C = B
6 2 5 mpbird φ C ran F