Definition df-f 4792

Description: Define a function (mapping) with domain and codomain. Definition 6.15(3) of [TakeutiZaring] p. 27. For alternate definitions, see dff2 5420, dff3 5421, and dff4 5422. (Contributed by SF, 5-Jan-2015.)

Assertion

Ref	Expression
df-f	|- (F:A-->B <-> (F Fn A /\ ran F C_ B))

Detailed syntax breakdown of Definition df-f

Step	Hyp	Ref	Expression
1		cA	. . 3 class A
2		cB	. . 3 class B
3		cF	. . 3 class F
4	1, 2, 3	wf 4778	. 2 wff F:A-->B
5	3, 1	wfn 4777	. . 3 wff F Fn A
6	3	crn 4774	. . . 4 class ran F
7	6, 2	wss 3258	. . 3 wff ran F C_ B
8	5, 7	wa 358	. 2 wff (F Fn A /\ ran F C_ B)
9	4, 8	wb 176	1 wff (F:A-->B <-> (F Fn A /\ ran F C_ B))

This definition is referenced by:  feq1  5211  feq2  5212  feq3  5213  nff  5222  ffn  5224  dffn2  5225  frn  5229  dffn3  5230  fss  5231  fco  5232  funssxp  5234  fun  5237  fnfco  5238  fssres  5239  fint  5246  fin  5247  f0  5249  fconst  5251  f1funfun  5264  fof  5270  dff1o2  5292  fun11iun  5306  ffoss  5315  dff2  5420  dff3  5421  ffnfv  5428  ffvresb  5432  fpr  5438  dff1o6  5476  fmpt  5693  fmpt2d  5696  mapexi  6004  map0e  6024  ovcelem1  6172  ceex  6175  fce  6189  sbthlem1  6204