Metamath Proof Explorer

Theorem dffn2

Description: Any function is a mapping into _V . (Contributed by NM, 31-Oct-1995) (Proof shortened by Andrew Salmon, 17-Sep-2011)

Ref Expression
Assertion dffn2 
|- ( F Fn A <-> F : A --> _V )

Proof

Step Hyp Ref Expression
1 ssv 
 |-  ran F C_ _V
2 1 biantru 
 |-  ( F Fn A <-> ( F Fn A /\ ran F C_ _V ) )
3 df-f 
 |-  ( F : A --> _V <-> ( F Fn A /\ ran F C_ _V ) )
4 2 3 bitr4i 
 |-  ( F Fn A <-> F : A --> _V )