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 \leftrightarrow F : A ⟶ V$

Step	Hyp	Ref	Expression
1		ssv	$⊢ ran F \subseteq V$
2	1	biantru	$⊢ F Fn A \leftrightarrow (F Fn A \land ran F \subseteq V)$
3		df-f	$⊢ F : A ⟶ V \leftrightarrow (F Fn A \land ran F \subseteq V)$
4	2 3	bitr4i	$⊢ F Fn A \leftrightarrow F : A ⟶ V$