Theorem fdm 6756

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

Syntax hints:   → wi 4   = wceq 1537  dom cdm 5700  ⟶wf 6569

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 6576  df-f 6577

This theorem is referenced by:  fdmd  6757  fdmi  6758  fimacnv  6769  fssxp  6775  ffdm  6777  f00  6803  f0dom0  6805  f0rn0  6806  fimadmfo  6843  fimadmfoALT  6845  focofo  6847  fimacnvOLD  7104  feldmfvelcdm  7120  dff3  7134  ffvresb  7159  dmfex  7945  fiun  7983  soseq  8200  fsuppeq  8216  fsuppeqg  8217  issmo2  8405  smoiso  8418  mapprc  8888  elpm2r  8903  map0b  8941  mapsnd  8944  brdomg  9016  brdomgOLD  9017  pw2f1olem  9142  iunmapdisj  10092  fodomfi2  10129  infmap2  10286  coftr  10342  fin23lem40  10420  isf34lem7  10448  axdc3lem2  10520  axdc3lem4  10522  rpnnen1lem4  13045  rpnnen1lem5  13046  fseqsupcl  14028  fseqsupubi  14029  ello12  15562  lo1bdd  15566  elo12  15573  o1bdd  15577  lo1o1  15578  rlimclim  15592  ramval  17055  0ram2  17068  0ramcl  17070  intopsn  18692  symgfixf1  19479  f1omvdconj  19488  pmtrdifellem1  19518  pmtrdifellem2  19519  gsumval3  19949  dprdss  20073  dmdprdsplitlem  20081  ablfaclem3  20131  evpmss  21627  pjdm2  21754  islindf2  21857  islindf4  21881  decpmatval  22792  pmatcollpw3lem  22810  iscnp3  23273  cnpnei  23293  cncls2  23302  cncls  23303  cnntr  23304  cncnp  23309  cndis  23320  paste  23323  cncmp  23421  imacmp  23426  hauscmplem  23435  cnconn  23451  kgencn  23585  xkopt  23684  xkococnlem  23688  fbasrn  23913  fmval  23972  fmf  23974  rnelfmlem  23981  rnelfm  23982  cnflf2  24032  psmetdmdm  24336  xmetres  24395  metres  24396  metcnp  24575  metustsym  24589  cfilucfil  24593  metuel2  24599  iscauf  25333  equivcau  25353  lmclimf  25357  ismbf  25682  ismbfcn  25683  mbfimaicc  25685  mbfimaopn2  25711  ibl0  25842  cniccibl  25896  cnicciblnc  25898  dvnfre  26010  c1liplem1  26055  c1lip2  26057  dvcnvrelem2  26077  plyco0  26251  plyeq0  26270  vieta1lem2  26371  ulm2  26446  ulmss  26458  ulmdvlem2  26462  ulmdvlem3  26463  itgulm  26469  basellem5  27146  nodmon  27713  eedimeq  28931  axcontlem10  29006  wlkn0  29657  wlkres  29706  wlkp1lem1  29709  pthdivtx  29765  dmadjrnb  31938  elnlfn  31960  xppreima  32664  symgcom2  33077  tocyc01  33111  tocyccntz  33137  elrspunidl  33421  smatrcl  33742  mdetpmtr1  33769  locfinreflem  33786  hauseqcn  33844  rge0scvg  33895  indpreima  33989  isrnmeas  34164  omsfval  34259  omscl  34260  omsf  34261  eulerpartlemv  34329  eulerpartlemd  34331  eulerpartlemb  34333  eulerpartlemr  34339  eulerpartlemgvv  34341  eulerpartlemgs2  34345  eulerpartlemn  34346  rpsqrtcn  34570  cvmlift2lem9  35279  cvmlift3lem7  35293  mrsubfval  35476  ivthALT  36301  curf  37558  uncf  37559  unccur  37563  matunitlindflem2  37577  ptrecube  37580  heicant  37615  mbfresfi  37626  itg2addnclem  37631  itg2addnclem2  37632  ftc1anclem1  37653  indexdom  37694  sdclem2  37702  cnres2  37723  sstotbnd2  37734  bnd2lem  37751  ismgmOLD  37810  ismndo2  37834  exidreslem  37837  rngosn3  37884  rngodm1dm2  37892  rhmqusspan  42142  coeq0i  42709  pw2f1ocnv  42994  cnioobibld  43175  dfno2  43390  fresin2  45079  evthiccabs  45414  dvsubcncf  45845  dvmulcncf  45846  dvdivcncf  45848  cnbdibl  45883  fourierdlem48  46075  fourierdlem49  46076  fourierdlem58  46085  fourierdlem59  46086  fourierdlem71  46098  fourierdlem73  46100  fourierdlem74  46101  fourierdlem75  46102  fourierdlem76  46103  fourierdlem80  46107  fourierdlem81  46108  fourierdlem89  46116  fourierdlem91  46118  fourierdlem92  46119  fourierdlem93  46120  fourierdlem94  46121  fourierdlem111  46138  fourierdlem112  46139  fourierdlem113  46140  fouriercn  46153  sge0val  46287  fge0iccico  46291  isomennd  46452  3f1oss1  46990  fafv2elrnb  47150  fmtnoinf  47410  nnsum4primeseven  47674  nnsum4primesevenALTV  47675  domnmsuppn0  48094  mndpsuppss  48096  scmsuppss  48097  fdivmpt  48274  fdivmptf  48275  refdivmptf  48276  fdivpm  48277  refdivpm  48278  elbigo2  48286  elbigolo1  48291