Definition df-f 6500

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 7049, dff3 7050, and dff4 7051. (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 6492	. 2 wff 𝐹:𝐴⟶𝐵
5	3, 1	wfn 6491	. . 3 wff 𝐹 Fn 𝐴
6	3	crn 5629	. . . 4 class ran 𝐹
7	6, 2	wss 3890	. . 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  6644  feq2  6645  feq3  6646  nff  6662  sbcfg  6664  ffn  6666  dffn2  6668  frn  6673  dffn3  6678  ffrnb  6680  fss  6682  fcof  6689  funssxp  6694  fdmrn  6697  fun  6700  fnfco  6703  fssres  6704  fcoi2  6713  fint  6717  fin  6718  f0  6719  fconst  6724  f1ssr  6740  fof  6750  dff1o2  6783  dff2  7049  dff3  7050  fmpt  7060  ffnfv  7069  ffvresb  7076  idref  7097  fpr  7105  dff1o6  7227  fliftf  7267  fiun  7893  f1iun  7894  ffoss  7896  1stcof  7969  2ndcof  7970  smores  8289  smores2  8291  iordsmo  8294  sbthlem9  9030  inf3lem6  9551  alephsmo  10021  alephsing  10195  axdc3lem2  10370  smobeth  10506  fpwwe2lem10  10560  gruiun  10719  gruima  10722  nqerf  10850  om2uzf1oi  13912  fclim  15512  invf  17732  funcres2b  17861  funcres2c  17867  hofcllem  18221  hofcl  18222  nfchnd  18574  gsumval2  18651  resmgmhm2b  18678  resmhm2b  18787  frmdss2  18828  gsumval3a  19875  subgdmdprd  20008  srgfcl  20174  lsslindf  21807  indlcim  21817  cnrest2  23248  lmss  23260  conncn  23388  txflf  23968  cnextf  24028  clsnsg  24072  tgpconncomp  24075  psmetxrge0  24275  causs  25262  ellimc2  25841  perfdvf  25867  c1lip2  25962  dvne0  25975  plyeq0  26173  plyreres  26246  aannenlem1  26291  taylf  26323  ulmss  26359  elno2  27615  elno3  27616  cutsf  27781  madef  27825  oniso  28260  mpteleeOLD  28961  ausgrusgrb  29231  ausgrumgri  29233  usgrexmplef  29325  subuhgr  29352  subupgr  29353  subumgr  29354  subusgr  29355  upgrres  29372  umgrres  29373  hhssnv  31332  pjfi  31772  maprnin  32801  cycpmconjslem1  33212  esplyfv1  33710  measdivcstALTV  34366  sitgf  34488  eulerpartlemn  34522  reprinrn  34759  cvmlift2lem9a  35482  satff  35589  icoreresf  37665  poimirlem30  37968  poimirlem31  37969  isbnd3  38102  dihf11lem  41709  ofoafg  43779  ofoaid1  43783  ofoaid2  43784  naddcnff  43787  ntrf  44547  clsf2  44550  gneispace3  44557  gneispacef2  44560  k0004lem1  44571  dvsid  44755  stoweidlem27  46452  stoweidlem29  46454  stoweidlem31  46456  fourierdlem15  46547  mbfresmf  47164  sinnpoly  47330  ffnafv  47610  fcdmvafv2v  47675  iccpartf  47882  slotresfo  49365