Definition df-f 6494

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 7042, dff3 7043, and dff4 7044. (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 6486	. 2 wff 𝐹:𝐴⟶𝐵
5	3, 1	wfn 6485	. . 3 wff 𝐹 Fn 𝐴
6	3	crn 5623	. . . 4 class ran 𝐹
7	6, 2	wss 3899	. . 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  6638  feq2  6639  feq3  6640  nff  6656  sbcfg  6658  ffn  6660  dffn2  6662  frn  6667  dffn3  6672  ffrnb  6674  fss  6676  fcof  6683  funssxp  6688  fdmrn  6691  fun  6694  fnfco  6697  fssres  6698  fcoi2  6707  fint  6711  fin  6712  f0  6713  fconst  6718  f1ssr  6734  fof  6744  dff1o2  6777  dff2  7042  dff3  7043  fmpt  7053  ffnfv  7062  ffvresb  7068  idref  7089  fpr  7097  dff1o6  7219  fliftf  7259  fiun  7885  f1iun  7886  ffoss  7888  1stcof  7961  2ndcof  7962  smores  8282  smores2  8284  iordsmo  8287  sbthlem9  9021  inf3lem6  9540  alephsmo  10010  alephsing  10184  axdc3lem2  10359  smobeth  10495  fpwwe2lem10  10549  gruiun  10708  gruima  10711  nqerf  10839  om2uzf1oi  13874  fclim  15474  invf  17690  funcres2b  17819  funcres2c  17825  hofcllem  18179  hofcl  18180  nfchnd  18532  gsumval2  18609  resmgmhm2b  18636  resmhm2b  18745  frmdss2  18786  gsumval3a  19830  subgdmdprd  19963  srgfcl  20129  lsslindf  21783  indlcim  21793  cnrest2  23228  lmss  23240  conncn  23368  txflf  23948  cnextf  24008  clsnsg  24052  tgpconncomp  24055  psmetxrge0  24255  causs  25252  ellimc2  25832  perfdvf  25858  c1lip2  25957  dvne0  25970  plyeq0  26170  plyreres  26244  aannenlem1  26290  taylf  26322  ulmss  26360  elno2  27620  elno3  27621  scutf  27780  madef  27824  onsiso  28236  mpteleeOLD  28917  ausgrusgrb  29187  ausgrumgri  29189  usgrexmplef  29281  subuhgr  29308  subupgr  29309  subumgr  29310  subusgr  29311  upgrres  29328  umgrres  29329  hhssnv  31288  pjfi  31728  maprnin  32759  cycpmconjslem1  33185  esplyfv1  33676  measdivcstALTV  34331  sitgf  34453  eulerpartlemn  34487  reprinrn  34724  cvmlift2lem9a  35446  satff  35553  icoreresf  37496  poimirlem30  37790  poimirlem31  37791  isbnd3  37924  dihf11lem  41465  ofoafg  43538  ofoaid1  43542  ofoaid2  43543  naddcnff  43546  ntrf  44306  clsf2  44309  gneispace3  44316  gneispacef2  44319  k0004lem1  44330  dvsid  44514  stoweidlem27  46213  stoweidlem29  46215  stoweidlem31  46217  fourierdlem15  46308  mbfresmf  46925  sinnpoly  47079  ffnafv  47359  fcdmvafv2v  47424  iccpartf  47619  slotresfo  49086