Theorem fdm 6749

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 6739	. 2 ⊢ (𝐹:𝐴⟶𝐵 → 𝐹 Fn 𝐴)
2	1	fndmd 6674	1 ⊢ (𝐹:𝐴⟶𝐵 → dom 𝐹 = 𝐴)

This proof depends on syntax axioms:   → wi 4   = wceq 1570  dom cdm 5658  ⟶wf 6562

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-fn 6569  df-f 6570

This theorem is used by:  fdmd  6750  fdmi  6751  fimacnv  6762  fssxp  6767  ffdm  6769  f00  6794  f0dom0  6796  f0rn0  6797  fimadmfo  6835  fimadmfoALT  6837  focofo  6839  feldmfvelcdm  7118  dff3  7132  ffvresb  7158  dmfex  7951  fiun  7989  soseq  8213  fsuppeq  8230  fsuppeqg  8231  issmo2  8395  smoiso  8408  mapprc  8889  elpm2r  8903  curf  8928  uncf  8929  map0b  8949  mapsnd  8952  brdomg  9023  pw2f1olem  9138  iunmapdisj  10141  fodomfi2  10178  infmap2  10334  coftr  10390  fin23lem40  10468  isf34lem7  10496  axdc3lem2  10568  axdc3lem4  10570  rpnnen1lem4  13148  rpnnen1lem5  13149  fseqsupcl  14160  fseqsupubi  14161  ello12  15727  lo1bdd  15731  elo12  15738  o1bdd  15742  lo1o1  15743  rlimclim  15757  ramval  17230  0ram2  17243  0ramcl  17245  intopsn  18882  mndpsuppss  19009  symgfixf1  19702  f1omvdconj  19711  pmtrdifellem1  19741  pmtrdifellem2  19742  gsumval3  20172  dprdss  20296  dmdprdsplitlem  20304  ablfaclem3  20354  evpmss  21947  pjdm2  22072  islindf2  22175  islindf4  22199  matunitlindflem2  23050  decpmatval  23138  pmatcollpw3lem  23156  iscnp3  23617  cnpnei  23637  cncls2  23646  cncls  23647  cnntr  23648  cncnp  23653  cndis  23664  paste  23667  cncmp  23765  imacmp  23770  hauscmplem  23779  cnconn  23795  kgencn  23930  xkopt  24029  xkococnlem  24033  fbasrn  24258  fmval  24317  fmf  24319  rnelfmlem  24326  rnelfm  24327  cnflf2  24377  psmetdmdm  24679  xmetres  24738  metres  24739  metcnp  24915  metustsym  24929  cfilucfil  24933  metuel2  24939  iscauf  25656  equivcau  25676  lmclimf  25680  ismbf  26004  ismbfcn  26005  mbfimaicc  26007  mbfimaopn2  26033  ibl0  26162  cniccibl  26216  cnicciblnc  26218  dvnfre  26327  c1liplem1  26371  c1lip2  26373  dvcnvrelem2  26393  plyco0  26565  plyeq0  26585  vieta1lem2  26689  ulm2  26769  ulmss  26781  ulmdvlem2  26785  ulmdvlem3  26786  itgulm  26792  basellem5  27469  nodmon  28064  newbdayim  28346  eedimeq  29533  axcontlem10  29608  wlkn0  30258  wlkres  30306  wlkp1lem1  30309  pthdivtx  30369  cyclnumvtx  30445  dmadjrnb  32565  elnlfn  32587  xppreima  33337  indpreima  33528  symgcom2  33744  tocyc01  33778  tocyccntz  33804  elrspunidl  34082  smatrcl  34539  mdetpmtr1  34566  locfinreflem  34583  hauseqcn  34641  rge0scvg  34692  isrnmeas  34944  omsfval  35037  omscl  35038  omsf  35039  eulerpartlemv  35107  eulerpartlemd  35109  eulerpartlemb  35111  eulerpartlemr  35117  eulerpartlemgvv  35119  eulerpartlemgs2  35123  eulerpartlemn  35124  rpsqrtcn  35333  cvmlift2lem9  36284  cvmlift3lem7  36298  mrsubfval  36481  ivthALT  37338  nvo2  38229  unccur  38794  ptrecube  38806  heicant  38841  mbfresfi  38852  itg2addnclem  38857  itg2addnclem2  38858  ftc1anclem1  38879  indexdom  38936  sdclem2  38942  cnres2  38963  sstotbnd2  38974  bnd2lem  38991  ismgmOLD  39050  ismndo2  39074  exidreslem  39077  rngosn3  39124  rngodm1dm2  39132  rhmqusspan  43501  coeq0i  44030  pw2f1ocnv  44310  cnioobibld  44477  dfno2  44690  fresin2  46460  evthiccabs  46781  dvsubcncf  47207  dvmulcncf  47208  dvdivcncf  47210  cnbdibl  47245  fourierdlem48  47437  fourierdlem49  47438  fourierdlem58  47447  fourierdlem59  47448  fourierdlem71  47460  fourierdlem73  47462  fourierdlem74  47463  fourierdlem75  47464  fourierdlem76  47465  fourierdlem80  47469  fourierdlem81  47470  fourierdlem89  47478  fourierdlem91  47480  fourierdlem92  47481  fourierdlem93  47482  fourierdlem94  47483  fourierdlem111  47500  fourierdlem112  47501  fourierdlem113  47502  fouriercn  47515  sge0val  47649  fge0iccico  47653  isomennd  47814  tannpoly  48213  3f1oss1  48418  fafv2elrnb  48578  fmtnoinf  48894  nnsum4primeseven  49171  nnsum4primesevenALTV  49172  upgrimwlklem2  49269  upgrimwlklem3  49270  upgrimtrlslem2  49276  cycl3grtri  49318  domnmsuppn0  49812  scmsuppss  49814  fdivmpt  49983  fdivmptf  49984  refdivmptf  49985  fdivpm  49986  refdivpm  49987  elbigo2  49995  elbigolo1  50000  xpco2  50299