Theorem fdm 6715

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

Syntax hints:   → wi 4   = wceq 1570  dom cdm 5661  ⟶wf 6532

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 210  df-an 401  df-fn 6539  df-f 6540

This theorem is referenced by:  fdmd  6716  fdmi  6717  fimacnv  6728  fssxp  6733  ffdm  6735  f00  6760  f0dom0  6762  f0rn0  6763  fimadmfo  6801  fimadmfoALT  6803  focofo  6805  feldmfvelcdm  7081  dff3  7095  ffvresb  7121  dmfex  7898  fiun  7936  soseq  8151  fsuppeq  8167  fsuppeqg  8168  issmo2  8332  smoiso  8345  mapprc  8824  elpm2r  8838  map0b  8877  mapsnd  8880  brdomg  8951  pw2f1olem  9065  iunmapdisj  10003  fodomfi2  10040  infmap2  10196  coftr  10252  fin23lem40  10330  isf34lem7  10358  axdc3lem2  10430  axdc3lem4  10432  rpnnen1lem4  12999  rpnnen1lem5  13000  fseqsupcl  14009  fseqsupubi  14010  ello12  15563  lo1bdd  15567  elo12  15574  o1bdd  15578  lo1o1  15579  rlimclim  15593  ramval  17063  0ram2  17076  0ramcl  17078  intopsn  18707  mndpsuppss  18818  symgfixf1  19502  f1omvdconj  19511  pmtrdifellem1  19541  pmtrdifellem2  19542  gsumval3  19972  dprdss  20096  dmdprdsplitlem  20104  ablfaclem3  20154  evpmss  21736  pjdm2  21861  islindf2  21964  islindf4  21988  decpmatval  22922  pmatcollpw3lem  22940  iscnp3  23401  cnpnei  23421  cncls2  23430  cncls  23431  cnntr  23432  cncnp  23437  cndis  23448  paste  23451  cncmp  23549  imacmp  23554  hauscmplem  23563  cnconn  23579  kgencn  23713  xkopt  23812  xkococnlem  23816  fbasrn  24041  fmval  24100  fmf  24102  rnelfmlem  24109  rnelfm  24110  cnflf2  24160  psmetdmdm  24462  xmetres  24521  metres  24522  metcnp  24698  metustsym  24712  cfilucfil  24716  metuel2  24722  iscauf  25439  equivcau  25459  lmclimf  25463  ismbf  25787  ismbfcn  25788  mbfimaicc  25790  mbfimaopn2  25816  ibl0  25946  cniccibl  26000  cnicciblnc  26002  dvnfre  26111  c1liplem1  26155  c1lip2  26157  dvcnvrelem2  26177  plyco0  26349  plyeq0  26368  vieta1lem2  26472  ulm2  26548  ulmss  26560  ulmdvlem2  26564  ulmdvlem3  26565  itgulm  26571  basellem5  27249  nodmon  27814  newbdayim  28096  eedimeq  29248  axcontlem10  29323  wlkn0  29970  wlkres  30018  wlkp1lem1  30021  pthdivtx  30076  cyclnumvtx  30149  dmadjrnb  32258  elnlfn  32280  xppreima  32990  indpreima  33185  symgcom2  33404  tocyc01  33438  tocyccntz  33464  elrspunidl  33736  smatrcl  34186  mdetpmtr1  34213  locfinreflem  34230  hauseqcn  34288  rge0scvg  34339  isrnmeas  34590  omsfval  34684  omscl  34685  omsf  34686  eulerpartlemv  34754  eulerpartlemd  34756  eulerpartlemb  34758  eulerpartlemr  34764  eulerpartlemgvv  34766  eulerpartlemgs2  34770  eulerpartlemn  34771  rpsqrtcn  34980  cvmlift2lem9  35803  cvmlift3lem7  35817  mrsubfval  36000  ivthALT  36846  curf  38249  uncf  38250  unccur  38254  matunitlindflem2  38268  ptrecube  38271  heicant  38306  mbfresfi  38317  itg2addnclem  38322  itg2addnclem2  38323  ftc1anclem1  38344  indexdom  38385  sdclem2  38393  cnres2  38414  sstotbnd2  38425  bnd2lem  38442  ismgmOLD  38501  ismndo2  38525  exidreslem  38528  rngosn3  38575  rngodm1dm2  38583  rhmqusspan  42952  coeq0i  43484  pw2f1ocnv  43764  cnioobibld  43941  dfno2  44154  fresin2  45890  evthiccabs  46212  dvsubcncf  46638  dvmulcncf  46639  dvdivcncf  46641  cnbdibl  46676  fourierdlem48  46868  fourierdlem49  46869  fourierdlem58  46878  fourierdlem59  46879  fourierdlem71  46891  fourierdlem73  46893  fourierdlem74  46894  fourierdlem75  46895  fourierdlem76  46896  fourierdlem80  46900  fourierdlem81  46901  fourierdlem89  46909  fourierdlem91  46911  fourierdlem92  46912  fourierdlem93  46913  fourierdlem94  46914  fourierdlem111  46931  fourierdlem112  46932  fourierdlem113  46933  fouriercn  46946  sge0val  47080  fge0iccico  47084  isomennd  47245  tannpoly  47627  3f1oss1  47812  fafv2elrnb  47972  fmtnoinf  48288  nnsum4primeseven  48565  nnsum4primesevenALTV  48566  upgrimwlklem2  48663  upgrimwlklem3  48664  upgrimtrlslem2  48670  cycl3grtri  48712  domnmsuppn0  49149  scmsuppss  49151  fdivmpt  49320  fdivmptf  49321  refdivmptf  49322  fdivpm  49323  refdivpm  49324  elbigo2  49332  elbigolo1  49337  xpco2  49635