Definition df-f 6544

Description: Define a function (mapping) with domain and codomain. Definition 6.15(3) of [TakeutiZaring] p. 27. 𝐹:𝐴⟶𝐵 can be read as "𝐹 is a function from 𝐴 to 𝐵". For alternate definitions, see dff2 7096, dff3 7097, and dff4 7098. (Contributed by NM, 1-Aug-1994.)

Assertion

Ref	Expression
df-f	⊢ (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵))

Detailed syntax breakdown of Definition df-f

Step	Hyp	Ref	Expression
1		cA	. . 3 class 𝐴
2		cB	. . 3 class 𝐵
3		cF	. . 3 class 𝐹
4	1, 2, 3	wf 6536	. 2 wff 𝐹:𝐴⟶𝐵
5	3, 1	wfn 6535	. . 3 wff 𝐹 Fn 𝐴
6	3	crn 5676	. . . 4 class ran 𝐹
7	6, 2	wss 3947	. . 3 wff ran 𝐹 ⊆ 𝐵
8	5, 7	wa 397	. 2 wff (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵)
9	4, 8	wb 205	1 wff (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵))

This definition is referenced by:  feq1  6695  feq2  6696  feq3  6697  nff  6710  sbcfg  6712  ffn  6714  dffn2  6716  frn  6721  dffn3  6727  ffrnb  6729  fss  6731  fcof  6737  fcoOLD  6739  funssxp  6743  fdmrn  6746  fun  6750  fnfco  6753  fssres  6754  fcoi2  6763  fint  6767  fin  6768  f0  6769  fconst  6774  f1ssr  6791  fof  6802  dff1o2  6835  dff2  7096  dff3  7097  fmpt  7105  ffnfv  7113  ffvresb  7119  idref  7139  fpr  7147  dff1o6  7268  fliftf  7307  fiun  7924  f1iun  7925  ffoss  7927  1stcof  8000  2ndcof  8001  smores  8347  smores2  8349  iordsmo  8352  sbthlem9  9087  inf3lem6  9624  alephsmo  10093  alephsing  10267  axdc3lem2  10442  smobeth  10577  fpwwe2lem10  10631  gruiun  10790  gruima  10793  nqerf  10921  om2uzf1oi  13914  fclim  15493  invf  17711  funcres2b  17843  funcres2c  17848  hofcllem  18207  hofcl  18208  gsumval2  18601  resmhm2b  18699  frmdss2  18740  gsumval3a  19763  subgdmdprd  19896  srgfcl  20010  lsslindf  21369  indlcim  21379  cnrest2  22772  lmss  22784  conncn  22912  txflf  23492  cnextf  23552  clsnsg  23596  tgpconncomp  23599  psmetxrge0  23801  causs  24797  ellimc2  25376  perfdvf  25402  c1lip2  25497  dvne0  25510  plyeq0  25707  plyreres  25778  aannenlem1  25823  taylf  25855  ulmss  25891  elno2  27137  elno3  27138  scutf  27293  madef  27331  mptelee  28133  ausgrusgrb  28405  ausgrumgri  28407  usgrexmplef  28496  subuhgr  28523  subupgr  28524  subumgr  28525  subusgr  28526  upgrres  28543  umgrres  28544  hhssnv  30495  pjfi  30935  maprnin  31934  cycpmconjslem1  32291  measdivcstALTV  33161  sitgf  33284  eulerpartlemn  33318  reprinrn  33568  cvmlift2lem9a  34232  satff  34339  icoreresf  36171  poimirlem30  36456  poimirlem31  36457  isbnd3  36590  dihf11lem  40075  ofoafg  42037  ofoaid1  42041  ofoaid2  42042  naddcnff  42045  ntrf  42807  clsf2  42810  gneispace3  42817  gneispacef2  42820  k0004lem1  42831  dvsid  43023  stoweidlem27  44678  stoweidlem29  44680  stoweidlem31  44682  fourierdlem15  44773  mbfresmf  45390  ffnafv  45814  fcdmvafv2v  45879  iccpartf  46034  resmgmhm2b  46505