Theorem fdm 6701

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

Syntax hints:   → wi 4   = wceq 1560  dom cdm 5647  ⟶wf 6517

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 209  df-an 400  df-fn 6524  df-f 6525

This theorem is referenced by:  fdmd  6702  fdmi  6703  fimacnv  6714  fssxp  6719  ffdm  6721  f00  6746  f0dom0  6748  f0rn0  6749  fimadmfo  6787  fimadmfoALT  6789  focofo  6791  feldmfvelcdm  7067  dff3  7081  ffvresb  7107  dmfex  7886  fiun  7924  soseq  8139  fsuppeq  8155  fsuppeqg  8156  issmo2  8320  smoiso  8333  mapprc  8812  elpm2r  8826  map0b  8865  mapsnd  8868  brdomg  8939  pw2f1olem  9053  iunmapdisj  9979  fodomfi2  10016  infmap2  10173  coftr  10230  fin23lem40  10308  isf34lem7  10336  axdc3lem2  10408  axdc3lem4  10410  rpnnen1lem4  12981  rpnnen1lem5  12982  fseqsupcl  13990  fseqsupubi  13991  ello12  15543  lo1bdd  15547  elo12  15554  o1bdd  15558  lo1o1  15559  rlimclim  15573  ramval  17044  0ram2  17057  0ramcl  17059  intopsn  18688  mndpsuppss  18799  symgfixf1  19477  f1omvdconj  19486  pmtrdifellem1  19516  pmtrdifellem2  19517  gsumval3  19947  dprdss  20071  dmdprdsplitlem  20079  ablfaclem3  20129  evpmss  21635  pjdm2  21760  islindf2  21863  islindf4  21887  decpmatval  22822  pmatcollpw3lem  22840  iscnp3  23301  cnpnei  23321  cncls2  23330  cncls  23331  cnntr  23332  cncnp  23337  cndis  23348  paste  23351  cncmp  23449  imacmp  23454  hauscmplem  23463  cnconn  23479  kgencn  23613  xkopt  23712  xkococnlem  23716  fbasrn  23941  fmval  24000  fmf  24002  rnelfmlem  24009  rnelfm  24010  cnflf2  24060  psmetdmdm  24362  xmetres  24421  metres  24422  metcnp  24598  metustsym  24612  cfilucfil  24616  metuel2  24622  iscauf  25339  equivcau  25359  lmclimf  25363  ismbf  25687  ismbfcn  25688  mbfimaicc  25690  mbfimaopn2  25716  ibl0  25846  cniccibl  25900  cnicciblnc  25902  dvnfre  26011  c1liplem1  26055  c1lip2  26057  dvcnvrelem2  26077  plyco0  26249  plyeq0  26268  vieta1lem2  26372  ulm2  26445  ulmss  26457  ulmdvlem2  26461  ulmdvlem3  26462  itgulm  26468  basellem5  27146  nodmon  27711  newbdayim  27993  eedimeq  29096  axcontlem10  29171  wlkn0  29818  wlkres  29866  wlkp1lem1  29869  pthdivtx  29924  cyclnumvtx  29997  dmadjrnb  32106  elnlfn  32128  xppreima  32844  indpreima  33040  symgcom2  33261  tocyc01  33295  tocyccntz  33321  elrspunidl  33611  smatrcl  34090  mdetpmtr1  34117  locfinreflem  34134  hauseqcn  34192  rge0scvg  34243  isrnmeas  34494  omsfval  34588  omscl  34589  omsf  34590  eulerpartlemv  34658  eulerpartlemd  34660  eulerpartlemb  34662  eulerpartlemr  34668  eulerpartlemgvv  34670  eulerpartlemgs2  34674  eulerpartlemn  34675  rpsqrtcn  34884  cvmlift2lem9  35658  cvmlift3lem7  35672  mrsubfval  35855  ivthALT  36692  curf  38094  uncf  38095  unccur  38099  matunitlindflem2  38113  ptrecube  38116  heicant  38151  mbfresfi  38162  itg2addnclem  38167  itg2addnclem2  38168  ftc1anclem1  38189  indexdom  38230  sdclem2  38238  cnres2  38259  sstotbnd2  38270  bnd2lem  38287  ismgmOLD  38346  ismndo2  38370  exidreslem  38373  rngosn3  38420  rngodm1dm2  38428  rhmqusspan  42799  coeq0i  43331  pw2f1ocnv  43611  cnioobibld  43788  dfno2  44001  fresin2  45747  evthiccabs  46069  dvsubcncf  46495  dvmulcncf  46496  dvdivcncf  46498  cnbdibl  46533  fourierdlem48  46725  fourierdlem49  46726  fourierdlem58  46735  fourierdlem59  46736  fourierdlem71  46748  fourierdlem73  46750  fourierdlem74  46751  fourierdlem75  46752  fourierdlem76  46753  fourierdlem80  46757  fourierdlem81  46758  fourierdlem89  46766  fourierdlem91  46768  fourierdlem92  46769  fourierdlem93  46770  fourierdlem94  46771  fourierdlem111  46788  fourierdlem112  46789  fourierdlem113  46790  fouriercn  46803  sge0val  46937  fge0iccico  46941  isomennd  47102  tannpoly  47481  3f1oss1  47666  fafv2elrnb  47826  fmtnoinf  48142  nnsum4primeseven  48419  nnsum4primesevenALTV  48420  upgrimwlklem2  48517  upgrimwlklem3  48518  upgrimtrlslem2  48524  cycl3grtri  48566  domnmsuppn0  48988  scmsuppss  48990  fdivmpt  49159  fdivmptf  49160  refdivmptf  49161  fdivpm  49162  refdivpm  49163  elbigo2  49171  elbigolo1  49176  xpco2  49475