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 <-> ( F Fn A /\ ran F C_ B ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cF	|- F
1		cA	|- A
2		cB	|- B
3	1 2 0	wf	|- F : A --> B
4	0 1	wfn	|- F Fn A
5	0	crn	|- ran F
6	5 2	wss	|- ran F C_ B
7	4 6	wa	|- ( F Fn A /\ ran F C_ B )
8	3 7	wb	|- ( F : A --> B <-> ( F Fn A /\ ran F C_ B ) )