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 C_ ran F
2 1 biantru 
 |-  ( F Fn A <-> ( F Fn A /\ ran F C_ ran F ) )
3 df-f 
 |-  ( F : A --> ran F <-> ( F Fn A /\ ran F C_ ran F ) )
4 2 3 bitr4i 
 |-  ( F Fn A <-> F : A --> ran F )