Theorem fdm 6593

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

Syntax hints:   → wi 4   = wceq 1539  dom cdm 5580  ⟶wf 6414

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 396  df-fn 6421  df-f 6422

This theorem is referenced by:  fdmd  6595  fdmi  6596  fimacnv  6606  fssxp  6612  ffdm  6614  f00  6640  f0dom0  6642  f0rn0  6643  fimadmfo  6681  fimadmfoALT  6683  focofo  6685  fimacnvOLD  6930  dff3  6958  ffvresb  6980  dmfex  7728  fiun  7759  frnsuppeq  7962  frnsuppeqg  7963  suppssOLD  7982  issmo2  8151  smoiso  8164  mapprc  8577  elpm2r  8591  map0b  8629  mapsnd  8632  brdomg  8703  pw2f1olem  8816  iunmapdisj  9710  fodomfi2  9747  infmap2  9905  coftr  9960  fin23lem40  10038  isf34lem7  10066  axdc3lem2  10138  axdc3lem4  10140  rpnnen1lem4  12649  rpnnen1lem5  12650  fseqsupcl  13625  fseqsupubi  13626  ello12  15153  lo1bdd  15157  elo12  15164  o1bdd  15168  lo1o1  15169  rlimclim  15183  ramval  16637  0ram2  16650  0ramcl  16652  intopsn  18253  symgfixf1  18960  f1omvdconj  18969  pmtrdifellem1  18999  pmtrdifellem2  19000  gsumval3  19423  dprdss  19547  dmdprdsplitlem  19555  ablfaclem3  19605  evpmss  20703  pjdm2  20828  islindf2  20931  islindf4  20955  decpmatval  21822  pmatcollpw3lem  21840  iscnp3  22303  cnpnei  22323  cncls2  22332  cncls  22333  cnntr  22334  cncnp  22339  cndis  22350  paste  22353  cncmp  22451  imacmp  22456  hauscmplem  22465  cnconn  22481  kgencn  22615  xkopt  22714  xkococnlem  22718  fbasrn  22943  fmval  23002  fmf  23004  rnelfmlem  23011  rnelfm  23012  cnflf2  23062  psmetdmdm  23366  xmetres  23425  metres  23426  metcnp  23603  metustsym  23617  cfilucfil  23621  metuel2  23627  iscauf  24349  equivcau  24369  lmclimf  24373  ismbf  24697  ismbfcn  24698  mbfimaicc  24700  mbfimaopn2  24726  ibl0  24856  cniccibl  24910  cnicciblnc  24912  dvnfre  25021  c1liplem1  25065  c1lip2  25067  dvcnvrelem2  25087  plyco0  25258  plyeq0  25277  vieta1lem2  25376  ulm2  25449  ulmss  25461  ulmdvlem2  25465  ulmdvlem3  25466  itgulm  25472  basellem5  26139  eedimeq  27169  axcontlem10  27244  wlkn0  27890  wlkres  27940  wlkp1lem1  27943  pthdivtx  27998  dmadjrnb  30169  elnlfn  30191  xppreima  30884  symgcom2  31255  tocyc01  31287  tocyccntz  31313  elrspunidl  31508  smatrcl  31648  mdetpmtr1  31675  locfinreflem  31692  hauseqcn  31750  rge0scvg  31801  indpreima  31893  isrnmeas  32068  omsfval  32161  omscl  32162  omsf  32163  eulerpartlemv  32231  eulerpartlemd  32233  eulerpartlemb  32235  eulerpartlemr  32241  eulerpartlemgvv  32243  eulerpartlemgs2  32247  eulerpartlemn  32248  rpsqrtcn  32473  cvmlift2lem9  33173  cvmlift3lem7  33187  mrsubfval  33370  soseq  33730  nodmon  33780  ivthALT  34451  curf  35682  uncf  35683  unccur  35687  matunitlindflem2  35701  ptrecube  35704  heicant  35739  mbfresfi  35750  itg2addnclem  35755  itg2addnclem2  35756  ftc1anclem1  35777  indexdom  35819  sdclem2  35827  cnres2  35848  sstotbnd2  35859  bnd2lem  35876  ismgmOLD  35935  ismndo2  35959  exidreslem  35962  rngosn3  36009  rngodm1dm2  36017  coeq0i  40491  pw2f1ocnv  40775  cnioobibld  40961  fresin2  42597  evthiccabs  42924  dvsubcncf  43355  dvmulcncf  43356  dvdivcncf  43358  cnbdibl  43393  fourierdlem48  43585  fourierdlem49  43586  fourierdlem58  43595  fourierdlem59  43596  fourierdlem71  43608  fourierdlem73  43610  fourierdlem74  43611  fourierdlem75  43612  fourierdlem76  43613  fourierdlem80  43617  fourierdlem81  43618  fourierdlem89  43626  fourierdlem91  43628  fourierdlem92  43629  fourierdlem93  43630  fourierdlem94  43631  fourierdlem111  43648  fourierdlem112  43649  fourierdlem113  43650  fouriercn  43663  sge0val  43794  fge0iccico  43798  isomennd  43959  fafv2elrnb  44614  fmtnoinf  44876  nnsum4primeseven  45140  nnsum4primesevenALTV  45141  domnmsuppn0  45593  mndpsuppss  45595  scmsuppss  45596  fdivmpt  45774  fdivmptf  45775  refdivmptf  45776  fdivpm  45777  refdivpm  45778  elbigo2  45786  elbigolo1  45791