Definition df-f 6497

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 7046, dff3 7047, and dff4 7048. (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 6489	. 2 wff 𝐹:𝐴⟶𝐵
5	3, 1	wfn 6488	. . 3 wff 𝐹 Fn 𝐴
6	3	crn 5626	. . . 4 class ran 𝐹
7	6, 2	wss 3902	. . 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  6641  feq2  6642  feq3  6643  nff  6659  sbcfg  6661  ffn  6663  dffn2  6665  frn  6670  dffn3  6675  ffrnb  6677  fss  6679  fcof  6686  funssxp  6691  fdmrn  6694  fun  6697  fnfco  6700  fssres  6701  fcoi2  6710  fint  6714  fin  6715  f0  6716  fconst  6721  f1ssr  6737  fof  6747  dff1o2  6780  dff2  7046  dff3  7047  fmpt  7057  ffnfv  7066  ffvresb  7072  idref  7093  fpr  7101  dff1o6  7223  fliftf  7263  fiun  7889  f1iun  7890  ffoss  7892  1stcof  7965  2ndcof  7966  smores  8286  smores2  8288  iordsmo  8291  sbthlem9  9027  inf3lem6  9546  alephsmo  10016  alephsing  10190  axdc3lem2  10365  smobeth  10501  fpwwe2lem10  10555  gruiun  10714  gruima  10717  nqerf  10845  om2uzf1oi  13880  fclim  15480  invf  17696  funcres2b  17825  funcres2c  17831  hofcllem  18185  hofcl  18186  nfchnd  18538  gsumval2  18615  resmgmhm2b  18642  resmhm2b  18751  frmdss2  18792  gsumval3a  19836  subgdmdprd  19969  srgfcl  20135  lsslindf  21789  indlcim  21799  cnrest2  23234  lmss  23246  conncn  23374  txflf  23954  cnextf  24014  clsnsg  24058  tgpconncomp  24061  psmetxrge0  24261  causs  25258  ellimc2  25838  perfdvf  25864  c1lip2  25963  dvne0  25976  plyeq0  26176  plyreres  26250  aannenlem1  26296  taylf  26328  ulmss  26366  elno2  27626  elno3  27627  cutsf  27792  madef  27836  oniso  28271  mpteleeOLD  28972  ausgrusgrb  29242  ausgrumgri  29244  usgrexmplef  29336  subuhgr  29363  subupgr  29364  subumgr  29365  subusgr  29366  upgrres  29383  umgrres  29384  hhssnv  31343  pjfi  31783  maprnin  32812  cycpmconjslem1  33238  esplyfv1  33729  measdivcstALTV  34384  sitgf  34506  eulerpartlemn  34540  reprinrn  34777  cvmlift2lem9a  35499  satff  35606  icoreresf  37559  poimirlem30  37853  poimirlem31  37854  isbnd3  37987  dihf11lem  41594  ofoafg  43663  ofoaid1  43667  ofoaid2  43668  naddcnff  43671  ntrf  44431  clsf2  44434  gneispace3  44441  gneispacef2  44444  k0004lem1  44455  dvsid  44639  stoweidlem27  46338  stoweidlem29  46340  stoweidlem31  46342  fourierdlem15  46433  mbfresmf  47050  sinnpoly  47204  ffnafv  47484  fcdmvafv2v  47549  iccpartf  47744  slotresfo  49211