Theorem fdm 6618

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

Syntax hints:   → wi 4   = wceq 1539  dom cdm 5590  ⟶wf 6433

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 206  df-an 397  df-fn 6440  df-f 6441

This theorem is referenced by:  fdmd  6620  fdmi  6621  fimacnv  6631  fssxp  6637  ffdm  6639  f00  6665  f0dom0  6667  f0rn0  6668  fimadmfo  6706  fimadmfoALT  6708  focofo  6710  fimacnvOLD  6957  dff3  6985  ffvresb  7007  dmfex  7763  fiun  7794  frnsuppeq  8000  frnsuppeqg  8001  suppssOLD  8020  issmo2  8189  smoiso  8202  mapprc  8628  elpm2r  8642  map0b  8680  mapsnd  8683  brdomg  8755  brdomgOLD  8756  pw2f1olem  8872  iunmapdisj  9788  fodomfi2  9825  infmap2  9983  coftr  10038  fin23lem40  10116  isf34lem7  10144  axdc3lem2  10216  axdc3lem4  10218  rpnnen1lem4  12729  rpnnen1lem5  12730  fseqsupcl  13706  fseqsupubi  13707  ello12  15234  lo1bdd  15238  elo12  15245  o1bdd  15249  lo1o1  15250  rlimclim  15264  ramval  16718  0ram2  16731  0ramcl  16733  intopsn  18347  symgfixf1  19054  f1omvdconj  19063  pmtrdifellem1  19093  pmtrdifellem2  19094  gsumval3  19517  dprdss  19641  dmdprdsplitlem  19649  ablfaclem3  19699  evpmss  20800  pjdm2  20927  islindf2  21030  islindf4  21054  decpmatval  21923  pmatcollpw3lem  21941  iscnp3  22404  cnpnei  22424  cncls2  22433  cncls  22434  cnntr  22435  cncnp  22440  cndis  22451  paste  22454  cncmp  22552  imacmp  22557  hauscmplem  22566  cnconn  22582  kgencn  22716  xkopt  22815  xkococnlem  22819  fbasrn  23044  fmval  23103  fmf  23105  rnelfmlem  23112  rnelfm  23113  cnflf2  23163  psmetdmdm  23467  xmetres  23526  metres  23527  metcnp  23706  metustsym  23720  cfilucfil  23724  metuel2  23730  iscauf  24453  equivcau  24473  lmclimf  24477  ismbf  24801  ismbfcn  24802  mbfimaicc  24804  mbfimaopn2  24830  ibl0  24960  cniccibl  25014  cnicciblnc  25016  dvnfre  25125  c1liplem1  25169  c1lip2  25171  dvcnvrelem2  25191  plyco0  25362  plyeq0  25381  vieta1lem2  25480  ulm2  25553  ulmss  25565  ulmdvlem2  25569  ulmdvlem3  25570  itgulm  25576  basellem5  26243  eedimeq  27275  axcontlem10  27350  wlkn0  27997  wlkres  28047  wlkp1lem1  28050  pthdivtx  28106  dmadjrnb  30277  elnlfn  30299  xppreima  30992  symgcom2  31362  tocyc01  31394  tocyccntz  31420  elrspunidl  31615  smatrcl  31755  mdetpmtr1  31782  locfinreflem  31799  hauseqcn  31857  rge0scvg  31908  indpreima  32002  isrnmeas  32177  omsfval  32270  omscl  32271  omsf  32272  eulerpartlemv  32340  eulerpartlemd  32342  eulerpartlemb  32344  eulerpartlemr  32350  eulerpartlemgvv  32352  eulerpartlemgs2  32356  eulerpartlemn  32357  rpsqrtcn  32582  cvmlift2lem9  33282  cvmlift3lem7  33296  mrsubfval  33479  soseq  33812  nodmon  33862  ivthALT  34533  curf  35764  uncf  35765  unccur  35769  matunitlindflem2  35783  ptrecube  35786  heicant  35821  mbfresfi  35832  itg2addnclem  35837  itg2addnclem2  35838  ftc1anclem1  35859  indexdom  35901  sdclem2  35909  cnres2  35930  sstotbnd2  35941  bnd2lem  35958  ismgmOLD  36017  ismndo2  36041  exidreslem  36044  rngosn3  36091  rngodm1dm2  36099  coeq0i  40582  pw2f1ocnv  40866  cnioobibld  41052  fresin2  42715  evthiccabs  43041  dvsubcncf  43472  dvmulcncf  43473  dvdivcncf  43475  cnbdibl  43510  fourierdlem48  43702  fourierdlem49  43703  fourierdlem58  43712  fourierdlem59  43713  fourierdlem71  43725  fourierdlem73  43727  fourierdlem74  43728  fourierdlem75  43729  fourierdlem76  43730  fourierdlem80  43734  fourierdlem81  43735  fourierdlem89  43743  fourierdlem91  43745  fourierdlem92  43746  fourierdlem93  43747  fourierdlem94  43748  fourierdlem111  43765  fourierdlem112  43766  fourierdlem113  43767  fouriercn  43780  sge0val  43911  fge0iccico  43915  isomennd  44076  fafv2elrnb  44738  fmtnoinf  44999  nnsum4primeseven  45263  nnsum4primesevenALTV  45264  domnmsuppn0  45716  mndpsuppss  45718  scmsuppss  45719  fdivmpt  45897  fdivmptf  45898  refdivmptf  45899  fdivpm  45900  refdivpm  45901  elbigo2  45909  elbigolo1  45914