This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊆ V
2 1 biantru ⊢ F Fn A ↔ F Fn A ∧ ran ⁡ F ⊆ V
3 df-f ⊢ F : A ⟶ V ↔ F Fn A ∧ ran ⁡ F ⊆ V
4 2 3 bitr4i ⊢ F Fn A ↔ F : A ⟶ V