Theorem fdm 6671

Description: The domain of a mapping. (Contributed by NM, 2-Aug-1994.) (Proof shortened by Wolf Lammen, 29-May-2024.)

Assertion

Ref	Expression
fdm	⊢ (𝐹:𝐴⟶𝐵 → dom 𝐹 = 𝐴)

Proof of Theorem fdm

Step	Hyp	Ref	Expression
1		ffn 6662	. 2 ⊢ (𝐹:𝐴⟶𝐵 → 𝐹 Fn 𝐴)
2	1	fndmd 6597	1 ⊢ (𝐹:𝐴⟶𝐵 → dom 𝐹 = 𝐴)

Syntax hints:   → wi 4   = wceq 1541  dom cdm 5624  ⟶wf 6488

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 207  df-an 396  df-fn 6495  df-f 6496

This theorem is referenced by:  fdmd  6672  fdmi  6673  fimacnv  6684  fssxp  6689  ffdm  6691  f00  6716  f0dom0  6718  f0rn0  6719  fimadmfo  6755  fimadmfoALT  6757  focofo  6759  feldmfvelcdm  7031  dff3  7045  ffvresb  7070  dmfex  7847  fiun  7887  soseq  8101  fsuppeq  8117  fsuppeqg  8118  issmo2  8281  smoiso  8294  mapprc  8767  elpm2r  8782  map0b  8821  mapsnd  8824  brdomg  8895  pw2f1olem  9009  iunmapdisj  9933  fodomfi2  9970  infmap2  10127  coftr  10183  fin23lem40  10261  isf34lem7  10289  axdc3lem2  10361  axdc3lem4  10363  rpnnen1lem4  12893  rpnnen1lem5  12894  fseqsupcl  13900  fseqsupubi  13901  ello12  15439  lo1bdd  15443  elo12  15450  o1bdd  15454  lo1o1  15455  rlimclim  15469  ramval  16936  0ram2  16949  0ramcl  16951  intopsn  18579  mndpsuppss  18690  symgfixf1  19366  f1omvdconj  19375  pmtrdifellem1  19405  pmtrdifellem2  19406  gsumval3  19836  dprdss  19960  dmdprdsplitlem  19968  ablfaclem3  20018  evpmss  21541  pjdm2  21666  islindf2  21769  islindf4  21793  decpmatval  22709  pmatcollpw3lem  22727  iscnp3  23188  cnpnei  23208  cncls2  23217  cncls  23218  cnntr  23219  cncnp  23224  cndis  23235  paste  23238  cncmp  23336  imacmp  23341  hauscmplem  23350  cnconn  23366  kgencn  23500  xkopt  23599  xkococnlem  23603  fbasrn  23828  fmval  23887  fmf  23889  rnelfmlem  23896  rnelfm  23897  cnflf2  23947  psmetdmdm  24249  xmetres  24308  metres  24309  metcnp  24485  metustsym  24499  cfilucfil  24503  metuel2  24509  iscauf  25236  equivcau  25256  lmclimf  25260  ismbf  25585  ismbfcn  25586  mbfimaicc  25588  mbfimaopn2  25614  ibl0  25744  cniccibl  25798  cnicciblnc  25800  dvnfre  25912  c1liplem1  25957  c1lip2  25959  dvcnvrelem2  25979  plyco0  26153  plyeq0  26172  vieta1lem2  26275  ulm2  26350  ulmss  26362  ulmdvlem2  26366  ulmdvlem3  26367  itgulm  26373  basellem5  27051  nodmon  27618  newbdayim  27899  eedimeq  28971  axcontlem10  29046  wlkn0  29694  wlkres  29742  wlkp1lem1  29745  pthdivtx  29800  cyclnumvtx  29873  dmadjrnb  31981  elnlfn  32003  xppreima  32723  indpreima  32947  symgcom2  33166  tocyc01  33200  tocyccntz  33226  elrspunidl  33509  smatrcl  33953  mdetpmtr1  33980  locfinreflem  33997  hauseqcn  34055  rge0scvg  34106  isrnmeas  34357  omsfval  34451  omscl  34452  omsf  34453  eulerpartlemv  34521  eulerpartlemd  34523  eulerpartlemb  34525  eulerpartlemr  34531  eulerpartlemgvv  34533  eulerpartlemgs2  34537  eulerpartlemn  34538  rpsqrtcn  34750  cvmlift2lem9  35505  cvmlift3lem7  35519  mrsubfval  35702  ivthALT  36529  curf  37799  uncf  37800  unccur  37804  matunitlindflem2  37818  ptrecube  37821  heicant  37856  mbfresfi  37867  itg2addnclem  37872  itg2addnclem2  37873  ftc1anclem1  37894  indexdom  37935  sdclem2  37943  cnres2  37964  sstotbnd2  37975  bnd2lem  37992  ismgmOLD  38051  ismndo2  38075  exidreslem  38078  rngosn3  38125  rngodm1dm2  38133  rhmqusspan  42439  coeq0i  42995  pw2f1ocnv  43279  cnioobibld  43456  dfno2  43669  fresin2  45416  evthiccabs  45742  dvsubcncf  46168  dvmulcncf  46169  dvdivcncf  46171  cnbdibl  46206  fourierdlem48  46398  fourierdlem49  46399  fourierdlem58  46408  fourierdlem59  46409  fourierdlem71  46421  fourierdlem73  46423  fourierdlem74  46424  fourierdlem75  46425  fourierdlem76  46426  fourierdlem80  46430  fourierdlem81  46431  fourierdlem89  46439  fourierdlem91  46441  fourierdlem92  46442  fourierdlem93  46443  fourierdlem94  46444  fourierdlem111  46461  fourierdlem112  46462  fourierdlem113  46463  fouriercn  46476  sge0val  46610  fge0iccico  46614  isomennd  46775  tannpoly  47136  3f1oss1  47321  fafv2elrnb  47481  fmtnoinf  47782  nnsum4primeseven  48046  nnsum4primesevenALTV  48047  upgrimwlklem2  48144  upgrimwlklem3  48145  upgrimtrlslem2  48151  cycl3grtri  48193  domnmsuppn0  48615  scmsuppss  48617  fdivmpt  48786  fdivmptf  48787  refdivmptf  48788  fdivpm  48789  refdivpm  48790  elbigo2  48798  elbigolo1  48803  xpco2  49102