Metamath Proof Explorer


Theorem dffn3

Description: A function maps to its range. (Contributed by NM, 1-Sep-1999)

Ref Expression
Assertion dffn3 F Fn A F : A ran F

Proof

Step Hyp Ref Expression
1 ssid ran F ran F
2 1 biantru F Fn A F Fn A ran F ran F
3 df-f F : A ran F F Fn A ran F ran F
4 2 3 bitr4i F Fn A F : A ran F