Definition df-f 6490

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 7037, dff3 7038, and dff4 7039. (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 6482	. 2 wff 𝐹:𝐴⟶𝐵
5	3, 1	wfn 6481	. . 3 wff 𝐹 Fn 𝐴
6	3	crn 5624	. . . 4 class ran 𝐹
7	6, 2	wss 3905	. . 3 wff ran 𝐹 ⊆ 𝐵
8	5, 7	wa 395	. 2 wff (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵)
9	4, 8	wb 206	1 wff (𝐹:𝐴⟶𝐵 ↔ (𝐹 Fn 𝐴 ∧ ran 𝐹 ⊆ 𝐵))

This definition is referenced by:  feq1  6634  feq2  6635  feq3  6636  nff  6652  sbcfg  6654  ffn  6656  dffn2  6658  frn  6663  dffn3  6668  ffrnb  6670  fss  6672  fcof  6679  funssxp  6684  fdmrn  6687  fun  6690  fnfco  6693  fssres  6694  fcoi2  6703  fint  6707  fin  6708  f0  6709  fconst  6714  f1ssr  6730  fof  6740  dff1o2  6773  dff2  7037  dff3  7038  fmpt  7048  ffnfv  7057  ffvresb  7063  idref  7084  fpr  7092  dff1o6  7216  fliftf  7256  fiun  7885  f1iun  7886  ffoss  7888  1stcof  7961  2ndcof  7962  smores  8282  smores2  8284  iordsmo  8287  sbthlem9  9019  inf3lem6  9548  alephsmo  10015  alephsing  10189  axdc3lem2  10364  smobeth  10499  fpwwe2lem10  10553  gruiun  10712  gruima  10715  nqerf  10843  om2uzf1oi  13878  fclim  15478  invf  17693  funcres2b  17822  funcres2c  17828  hofcllem  18182  hofcl  18183  gsumval2  18578  resmgmhm2b  18605  resmhm2b  18714  frmdss2  18755  gsumval3a  19800  subgdmdprd  19933  srgfcl  20099  lsslindf  21755  indlcim  21765  cnrest2  23189  lmss  23201  conncn  23329  txflf  23909  cnextf  23969  clsnsg  24013  tgpconncomp  24016  psmetxrge0  24217  causs  25214  ellimc2  25794  perfdvf  25820  c1lip2  25919  dvne0  25932  plyeq0  26132  plyreres  26206  aannenlem1  26252  taylf  26284  ulmss  26322  elno2  27582  elno3  27583  scutf  27741  madef  27784  onsiso  28192  mptelee  28858  ausgrusgrb  29128  ausgrumgri  29130  usgrexmplef  29222  subuhgr  29249  subupgr  29250  subumgr  29251  subusgr  29252  upgrres  29269  umgrres  29270  hhssnv  31226  pjfi  31666  maprnin  32687  cycpmconjslem1  33109  measdivcstALTV  34194  sitgf  34317  eulerpartlemn  34351  reprinrn  34588  cvmlift2lem9a  35278  satff  35385  icoreresf  37328  poimirlem30  37632  poimirlem31  37633  isbnd3  37766  dihf11lem  41248  ofoafg  43330  ofoaid1  43334  ofoaid2  43335  naddcnff  43338  ntrf  44099  clsf2  44102  gneispace3  44109  gneispacef2  44112  k0004lem1  44123  dvsid  44307  stoweidlem27  46012  stoweidlem29  46014  stoweidlem31  46016  fourierdlem15  46107  mbfresmf  46724  sinnpoly  46879  ffnafv  47159  fcdmvafv2v  47224  iccpartf  47419  slotresfo  48887