Definition df-f 6548

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 7101, dff3 7102, and dff4 7103. (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 6540	. 2 wff 𝐹:𝐴⟶𝐵
5	3, 1	wfn 6539	. . 3 wff 𝐹 Fn 𝐴
6	3	crn 5678	. . . 4 class ran 𝐹
7	6, 2	wss 3949	. . 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  6699  feq2  6700  feq3  6701  nff  6714  sbcfg  6716  ffn  6718  dffn2  6720  frn  6725  dffn3  6731  ffrnb  6733  fss  6735  fcof  6741  fcoOLD  6743  funssxp  6747  fdmrn  6750  fun  6754  fnfco  6757  fssres  6758  fcoi2  6767  fint  6771  fin  6772  f0  6773  fconst  6778  f1ssr  6795  fof  6806  dff1o2  6839  dff2  7101  dff3  7102  fmpt  7110  ffnfv  7118  ffvresb  7124  idref  7144  fpr  7152  dff1o6  7273  fliftf  7312  fiun  7929  f1iun  7930  ffoss  7932  1stcof  8005  2ndcof  8006  smores  8352  smores2  8354  iordsmo  8357  sbthlem9  9091  inf3lem6  9628  alephsmo  10097  alephsing  10271  axdc3lem2  10446  smobeth  10581  fpwwe2lem10  10635  gruiun  10794  gruima  10797  nqerf  10925  om2uzf1oi  13918  fclim  15497  invf  17715  funcres2b  17847  funcres2c  17852  hofcllem  18211  hofcl  18212  gsumval2  18605  resmhm2b  18703  frmdss2  18744  gsumval3a  19771  subgdmdprd  19904  srgfcl  20019  lsslindf  21385  indlcim  21395  cnrest2  22790  lmss  22802  conncn  22930  txflf  23510  cnextf  23570  clsnsg  23614  tgpconncomp  23617  psmetxrge0  23819  causs  24815  ellimc2  25394  perfdvf  25420  c1lip2  25515  dvne0  25528  plyeq0  25725  plyreres  25796  aannenlem1  25841  taylf  25873  ulmss  25909  elno2  27157  elno3  27158  scutf  27313  madef  27351  mptelee  28153  ausgrusgrb  28425  ausgrumgri  28427  usgrexmplef  28516  subuhgr  28543  subupgr  28544  subumgr  28545  subusgr  28546  upgrres  28563  umgrres  28564  hhssnv  30517  pjfi  30957  maprnin  31956  cycpmconjslem1  32313  measdivcstALTV  33223  sitgf  33346  eulerpartlemn  33380  reprinrn  33630  cvmlift2lem9a  34294  satff  34401  icoreresf  36233  poimirlem30  36518  poimirlem31  36519  isbnd3  36652  dihf11lem  40137  ofoafg  42104  ofoaid1  42108  ofoaid2  42109  naddcnff  42112  ntrf  42874  clsf2  42877  gneispace3  42884  gneispacef2  42887  k0004lem1  42898  dvsid  43090  stoweidlem27  44743  stoweidlem29  44745  stoweidlem31  44747  fourierdlem15  44838  mbfresmf  45455  ffnafv  45879  fcdmvafv2v  45944  iccpartf  46099  resmgmhm2b  46570