Metamath Proof Explorer


Theorem dfrn4

Description: Range defined in terms of image. (Contributed by NM, 14-May-2008)

Ref Expression
Assertion dfrn4 ranA=AV

Proof

Step Hyp Ref Expression
1 df-ima AV=ranAV
2 rnresv ranAV=ranA
3 1 2 eqtr2i ranA=AV