Theorem fdm 6601

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

Syntax hints:   → wi 4   = wceq 1539  dom cdm 5584  ⟶wf 6422

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 6429  df-f 6430

This theorem is referenced by:  fdmd  6603  fdmi  6604  fimacnv  6614  fssxp  6620  ffdm  6622  f00  6648  f0dom0  6650  f0rn0  6651  fimadmfo  6689  fimadmfoALT  6691  focofo  6693  fimacnvOLD  6940  dff3  6968  ffvresb  6990  dmfex  7744  fiun  7775  frnsuppeq  7978  frnsuppeqg  7979  suppssOLD  7998  issmo2  8167  smoiso  8180  mapprc  8606  elpm2r  8620  map0b  8658  mapsnd  8661  brdomg  8733  brdomgOLD  8734  pw2f1olem  8850  iunmapdisj  9789  fodomfi2  9826  infmap2  9984  coftr  10039  fin23lem40  10117  isf34lem7  10145  axdc3lem2  10217  axdc3lem4  10219  rpnnen1lem4  12730  rpnnen1lem5  12731  fseqsupcl  13707  fseqsupubi  13708  ello12  15235  lo1bdd  15239  elo12  15246  o1bdd  15250  lo1o1  15251  rlimclim  15265  ramval  16719  0ram2  16732  0ramcl  16734  intopsn  18348  symgfixf1  19055  f1omvdconj  19064  pmtrdifellem1  19094  pmtrdifellem2  19095  gsumval3  19518  dprdss  19642  dmdprdsplitlem  19650  ablfaclem3  19700  evpmss  20801  pjdm2  20928  islindf2  21031  islindf4  21055  decpmatval  21924  pmatcollpw3lem  21942  iscnp3  22405  cnpnei  22425  cncls2  22434  cncls  22435  cnntr  22436  cncnp  22441  cndis  22452  paste  22455  cncmp  22553  imacmp  22558  hauscmplem  22567  cnconn  22583  kgencn  22717  xkopt  22816  xkococnlem  22820  fbasrn  23045  fmval  23104  fmf  23106  rnelfmlem  23113  rnelfm  23114  cnflf2  23164  psmetdmdm  23468  xmetres  23527  metres  23528  metcnp  23707  metustsym  23721  cfilucfil  23725  metuel2  23731  iscauf  24454  equivcau  24474  lmclimf  24478  ismbf  24802  ismbfcn  24803  mbfimaicc  24805  mbfimaopn2  24831  ibl0  24961  cniccibl  25015  cnicciblnc  25017  dvnfre  25126  c1liplem1  25170  c1lip2  25172  dvcnvrelem2  25192  plyco0  25363  plyeq0  25382  vieta1lem2  25481  ulm2  25554  ulmss  25566  ulmdvlem2  25570  ulmdvlem3  25571  itgulm  25577  basellem5  26244  eedimeq  27276  axcontlem10  27351  wlkn0  27997  wlkres  28047  wlkp1lem1  28050  pthdivtx  28105  dmadjrnb  30276  elnlfn  30298  xppreima  30991  symgcom2  31361  tocyc01  31393  tocyccntz  31419  elrspunidl  31614  smatrcl  31754  mdetpmtr1  31781  locfinreflem  31798  hauseqcn  31856  rge0scvg  31907  indpreima  32001  isrnmeas  32176  omsfval  32269  omscl  32270  omsf  32271  eulerpartlemv  32339  eulerpartlemd  32341  eulerpartlemb  32343  eulerpartlemr  32349  eulerpartlemgvv  32351  eulerpartlemgs2  32355  eulerpartlemn  32356  rpsqrtcn  32581  cvmlift2lem9  33281  cvmlift3lem7  33295  mrsubfval  33478  soseq  33811  nodmon  33861  ivthALT  34532  curf  35763  uncf  35764  unccur  35768  matunitlindflem2  35782  ptrecube  35785  heicant  35820  mbfresfi  35831  itg2addnclem  35836  itg2addnclem2  35837  ftc1anclem1  35858  indexdom  35900  sdclem2  35908  cnres2  35929  sstotbnd2  35940  bnd2lem  35957  ismgmOLD  36016  ismndo2  36040  exidreslem  36043  rngosn3  36090  rngodm1dm2  36098  coeq0i  40583  pw2f1ocnv  40867  cnioobibld  41053  fresin2  42689  evthiccabs  43015  dvsubcncf  43446  dvmulcncf  43447  dvdivcncf  43449  cnbdibl  43484  fourierdlem48  43676  fourierdlem49  43677  fourierdlem58  43686  fourierdlem59  43687  fourierdlem71  43699  fourierdlem73  43701  fourierdlem74  43702  fourierdlem75  43703  fourierdlem76  43704  fourierdlem80  43708  fourierdlem81  43709  fourierdlem89  43717  fourierdlem91  43719  fourierdlem92  43720  fourierdlem93  43721  fourierdlem94  43722  fourierdlem111  43739  fourierdlem112  43740  fourierdlem113  43741  fouriercn  43754  sge0val  43885  fge0iccico  43889  isomennd  44050  fafv2elrnb  44705  fmtnoinf  44966  nnsum4primeseven  45230  nnsum4primesevenALTV  45231  domnmsuppn0  45683  mndpsuppss  45685  scmsuppss  45686  fdivmpt  45864  fdivmptf  45865  refdivmptf  45866  fdivpm  45867  refdivpm  45868  elbigo2  45876  elbigolo1  45881