Metamath Proof Explorer

Definition df-f

Description: Define a function (mapping) with domain and codomain. Definition 6.15(3) of TakeutiZaring p. 27. F : A --> B can be read as " F is a function from A to B ". For alternate definitions, see dff2 , dff3 , and dff4 . (Contributed by NM, 1-Aug-1994)

		Ref	Expression
	Assertion	df-f	$⊢ F : A ⟶ B \leftrightarrow (F Fn A \land ran F \subseteq B)$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cF	$class F$
1		cA	$class A$
2		cB	$class B$
3	1 2 0	wf	$wff F : A ⟶ B$
4	0 1	wfn	$wff F Fn A$
5	0	crn	$class ran F$
6	5 2	wss	$wff ran F \subseteq B$
7	4 6	wa	$wff (F Fn A \land ran F \subseteq B)$
8	3 7	wb	$wff (F : A ⟶ B \leftrightarrow (F Fn A \land ran F \subseteq B))$