Theorem fdm 6682

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

Syntax hints:   → wi 4   = wceq 1541  dom cdm 5638  ⟶wf 6497

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 6504  df-f 6505

This theorem is referenced by:  fdmd  6684  fdmi  6685  fimacnv  6695  fssxp  6701  ffdm  6703  f00  6729  f0dom0  6731  f0rn0  6732  fimadmfo  6770  fimadmfoALT  6772  focofo  6774  fimacnvOLD  7026  dff3  7055  ffvresb  7077  dmfex  7849  fiun  7880  soseq  8096  fsuppeq  8111  fsuppeqg  8112  suppssOLD  8131  issmo2  8300  smoiso  8313  mapprc  8776  elpm2r  8790  map0b  8828  mapsnd  8831  brdomg  8903  brdomgOLD  8904  pw2f1olem  9027  iunmapdisj  9968  fodomfi2  10005  infmap2  10163  coftr  10218  fin23lem40  10296  isf34lem7  10324  axdc3lem2  10396  axdc3lem4  10398  rpnnen1lem4  12914  rpnnen1lem5  12915  fseqsupcl  13892  fseqsupubi  13893  ello12  15410  lo1bdd  15414  elo12  15421  o1bdd  15425  lo1o1  15426  rlimclim  15440  ramval  16891  0ram2  16904  0ramcl  16906  intopsn  18523  symgfixf1  19233  f1omvdconj  19242  pmtrdifellem1  19272  pmtrdifellem2  19273  gsumval3  19698  dprdss  19822  dmdprdsplitlem  19830  ablfaclem3  19880  evpmss  21027  pjdm2  21154  islindf2  21257  islindf4  21281  decpmatval  22151  pmatcollpw3lem  22169  iscnp3  22632  cnpnei  22652  cncls2  22661  cncls  22662  cnntr  22663  cncnp  22668  cndis  22679  paste  22682  cncmp  22780  imacmp  22785  hauscmplem  22794  cnconn  22810  kgencn  22944  xkopt  23043  xkococnlem  23047  fbasrn  23272  fmval  23331  fmf  23333  rnelfmlem  23340  rnelfm  23341  cnflf2  23391  psmetdmdm  23695  xmetres  23754  metres  23755  metcnp  23934  metustsym  23948  cfilucfil  23952  metuel2  23958  iscauf  24681  equivcau  24701  lmclimf  24705  ismbf  25029  ismbfcn  25030  mbfimaicc  25032  mbfimaopn2  25058  ibl0  25188  cniccibl  25242  cnicciblnc  25244  dvnfre  25353  c1liplem1  25397  c1lip2  25399  dvcnvrelem2  25419  plyco0  25590  plyeq0  25609  vieta1lem2  25708  ulm2  25781  ulmss  25793  ulmdvlem2  25797  ulmdvlem3  25798  itgulm  25804  basellem5  26471  nodmon  27035  eedimeq  27910  axcontlem10  27985  wlkn0  28632  wlkres  28681  wlkp1lem1  28684  pthdivtx  28740  dmadjrnb  30911  elnlfn  30933  xppreima  31629  symgcom2  32005  tocyc01  32037  tocyccntz  32063  elrspunidl  32279  smatrcl  32466  mdetpmtr1  32493  locfinreflem  32510  hauseqcn  32568  rge0scvg  32619  indpreima  32713  isrnmeas  32888  omsfval  32983  omscl  32984  omsf  32985  eulerpartlemv  33053  eulerpartlemd  33055  eulerpartlemb  33057  eulerpartlemr  33063  eulerpartlemgvv  33065  eulerpartlemgs2  33069  eulerpartlemn  33070  rpsqrtcn  33295  cvmlift2lem9  33992  cvmlift3lem7  34006  mrsubfval  34189  ivthALT  34883  curf  36129  uncf  36130  unccur  36134  matunitlindflem2  36148  ptrecube  36151  heicant  36186  mbfresfi  36197  itg2addnclem  36202  itg2addnclem2  36203  ftc1anclem1  36224  indexdom  36266  sdclem2  36274  cnres2  36295  sstotbnd2  36306  bnd2lem  36323  ismgmOLD  36382  ismndo2  36406  exidreslem  36409  rngosn3  36456  rngodm1dm2  36464  coeq0i  41134  pw2f1ocnv  41419  cnioobibld  41606  dfno2  41822  fresin2  43511  evthiccabs  43854  dvsubcncf  44285  dvmulcncf  44286  dvdivcncf  44288  cnbdibl  44323  fourierdlem48  44515  fourierdlem49  44516  fourierdlem58  44525  fourierdlem59  44526  fourierdlem71  44538  fourierdlem73  44540  fourierdlem74  44541  fourierdlem75  44542  fourierdlem76  44543  fourierdlem80  44547  fourierdlem81  44548  fourierdlem89  44556  fourierdlem91  44558  fourierdlem92  44559  fourierdlem93  44560  fourierdlem94  44561  fourierdlem111  44578  fourierdlem112  44579  fourierdlem113  44580  fouriercn  44593  sge0val  44727  fge0iccico  44731  isomennd  44892  fafv2elrnb  45587  fmtnoinf  45848  nnsum4primeseven  46112  nnsum4primesevenALTV  46113  domnmsuppn0  46565  mndpsuppss  46567  scmsuppss  46568  fdivmpt  46746  fdivmptf  46747  refdivmptf  46748  fdivpm  46749  refdivpm  46750  elbigo2  46758  elbigolo1  46763