Theorem fdm 6655

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

Syntax hints:   → wi 4   = wceq 1541  dom cdm 5611  ⟶wf 6472

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 6479  df-f 6480

This theorem is referenced by:  fdmd  6656  fdmi  6657  fimacnv  6668  fssxp  6673  ffdm  6675  f00  6700  f0dom0  6702  f0rn0  6703  fimadmfo  6739  fimadmfoALT  6741  focofo  6743  feldmfvelcdm  7014  dff3  7028  ffvresb  7053  dmfex  7830  fiun  7870  soseq  8084  fsuppeq  8100  fsuppeqg  8101  issmo2  8264  smoiso  8277  mapprc  8749  elpm2r  8764  map0b  8802  mapsnd  8805  brdomg  8876  pw2f1olem  8989  iunmapdisj  9909  fodomfi2  9946  infmap2  10103  coftr  10159  fin23lem40  10237  isf34lem7  10265  axdc3lem2  10337  axdc3lem4  10339  rpnnen1lem4  12873  rpnnen1lem5  12874  fseqsupcl  13879  fseqsupubi  13880  ello12  15418  lo1bdd  15422  elo12  15429  o1bdd  15433  lo1o1  15434  rlimclim  15448  ramval  16915  0ram2  16928  0ramcl  16930  intopsn  18557  mndpsuppss  18668  symgfixf1  19344  f1omvdconj  19353  pmtrdifellem1  19383  pmtrdifellem2  19384  gsumval3  19814  dprdss  19938  dmdprdsplitlem  19946  ablfaclem3  19996  evpmss  21518  pjdm2  21643  islindf2  21746  islindf4  21770  decpmatval  22675  pmatcollpw3lem  22693  iscnp3  23154  cnpnei  23174  cncls2  23183  cncls  23184  cnntr  23185  cncnp  23190  cndis  23201  paste  23204  cncmp  23302  imacmp  23307  hauscmplem  23316  cnconn  23332  kgencn  23466  xkopt  23565  xkococnlem  23569  fbasrn  23794  fmval  23853  fmf  23855  rnelfmlem  23862  rnelfm  23863  cnflf2  23913  psmetdmdm  24215  xmetres  24274  metres  24275  metcnp  24451  metustsym  24465  cfilucfil  24469  metuel2  24475  iscauf  25202  equivcau  25222  lmclimf  25226  ismbf  25551  ismbfcn  25552  mbfimaicc  25554  mbfimaopn2  25580  ibl0  25710  cniccibl  25764  cnicciblnc  25766  dvnfre  25878  c1liplem1  25923  c1lip2  25925  dvcnvrelem2  25945  plyco0  26119  plyeq0  26138  vieta1lem2  26241  ulm2  26316  ulmss  26328  ulmdvlem2  26332  ulmdvlem3  26333  itgulm  26339  basellem5  27017  nodmon  27584  newbdayim  27843  eedimeq  28871  axcontlem10  28946  wlkn0  29594  wlkres  29642  wlkp1lem1  29645  pthdivtx  29700  cyclnumvtx  29773  dmadjrnb  31878  elnlfn  31900  xppreima  32619  indpreima  32838  symgcom2  33045  tocyc01  33079  tocyccntz  33105  elrspunidl  33385  smatrcl  33801  mdetpmtr1  33828  locfinreflem  33845  hauseqcn  33903  rge0scvg  33954  isrnmeas  34205  omsfval  34299  omscl  34300  omsf  34301  eulerpartlemv  34369  eulerpartlemd  34371  eulerpartlemb  34373  eulerpartlemr  34379  eulerpartlemgvv  34381  eulerpartlemgs2  34385  eulerpartlemn  34386  rpsqrtcn  34598  cvmlift2lem9  35347  cvmlift3lem7  35361  mrsubfval  35544  ivthALT  36369  curf  37638  uncf  37639  unccur  37643  matunitlindflem2  37657  ptrecube  37660  heicant  37695  mbfresfi  37706  itg2addnclem  37711  itg2addnclem2  37712  ftc1anclem1  37733  indexdom  37774  sdclem2  37782  cnres2  37803  sstotbnd2  37814  bnd2lem  37831  ismgmOLD  37890  ismndo2  37914  exidreslem  37917  rngosn3  37964  rngodm1dm2  37972  rhmqusspan  42218  coeq0i  42786  pw2f1ocnv  43070  cnioobibld  43247  dfno2  43461  fresin2  45209  evthiccabs  45536  dvsubcncf  45962  dvmulcncf  45963  dvdivcncf  45965  cnbdibl  46000  fourierdlem48  46192  fourierdlem49  46193  fourierdlem58  46202  fourierdlem59  46203  fourierdlem71  46215  fourierdlem73  46217  fourierdlem74  46218  fourierdlem75  46219  fourierdlem76  46220  fourierdlem80  46224  fourierdlem81  46225  fourierdlem89  46233  fourierdlem91  46235  fourierdlem92  46236  fourierdlem93  46237  fourierdlem94  46238  fourierdlem111  46255  fourierdlem112  46256  fourierdlem113  46257  fouriercn  46270  sge0val  46404  fge0iccico  46408  isomennd  46569  tannpoly  46921  3f1oss1  47106  fafv2elrnb  47266  fmtnoinf  47567  nnsum4primeseven  47831  nnsum4primesevenALTV  47832  upgrimwlklem2  47929  upgrimwlklem3  47930  upgrimtrlslem2  47936  cycl3grtri  47978  domnmsuppn0  48400  scmsuppss  48402  fdivmpt  48572  fdivmptf  48573  refdivmptf  48574  fdivpm  48575  refdivpm  48576  elbigo2  48584  elbigolo1  48589  xpco2  48888