Definition df-f 4791

Description: Define a function (mapping) with domain and codomain. Definition 6.15(3) of [TakeutiZaring] p. 27. For alternate definitions, see dff2 5419, dff3 5420, and dff4 5421. (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 4777	. 2 wff F:A-->B
5	3, 1	wfn 4776	. . 3 wff F Fn A
6	3	crn 4773	. . . 4 class ran F
7	6, 2	wss 3257	. . 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  5210  feq2  5211  feq3  5212  nff  5221  ffn  5223  dffn2  5224  frn  5228  dffn3  5229  fss  5230  fco  5231  funssxp  5233  fun  5236  fnfco  5237  fssres  5238  fint  5245  fin  5246  f0  5248  fconst  5250  f1funfun  5263  fof  5269  dff1o2  5291  fun11iun  5305  ffoss  5314  dff2  5419  dff3  5420  ffnfv  5427  ffvresb  5431  fpr  5437  dff1o6  5475  fmpt  5692  fmpt2d  5695  mapexi  6003  map0e  6023  ovcelem1  6171  ceex  6174  fce  6188  sbthlem1  6203