Theorem fdm 6679

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

Syntax hints:   → wi 4   = wceq 1542  dom cdm 5632  ⟶wf 6496

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

This theorem is referenced by:  fdmd  6680  fdmi  6681  fimacnv  6692  fssxp  6697  ffdm  6699  f00  6724  f0dom0  6726  f0rn0  6727  fimadmfo  6763  fimadmfoALT  6765  focofo  6767  feldmfvelcdm  7040  dff3  7054  ffvresb  7080  dmfex  7858  fiun  7898  soseq  8111  fsuppeq  8127  fsuppeqg  8128  issmo2  8291  smoiso  8304  mapprc  8779  elpm2r  8794  map0b  8833  mapsnd  8836  brdomg  8907  pw2f1olem  9021  iunmapdisj  9947  fodomfi2  9984  infmap2  10141  coftr  10197  fin23lem40  10275  isf34lem7  10303  axdc3lem2  10375  axdc3lem4  10377  rpnnen1lem4  12932  rpnnen1lem5  12933  fseqsupcl  13941  fseqsupubi  13942  ello12  15480  lo1bdd  15484  elo12  15491  o1bdd  15495  lo1o1  15496  rlimclim  15510  ramval  16981  0ram2  16994  0ramcl  16996  intopsn  18624  mndpsuppss  18735  symgfixf1  19414  f1omvdconj  19423  pmtrdifellem1  19453  pmtrdifellem2  19454  gsumval3  19884  dprdss  20008  dmdprdsplitlem  20016  ablfaclem3  20066  evpmss  21568  pjdm2  21693  islindf2  21796  islindf4  21820  decpmatval  22732  pmatcollpw3lem  22750  iscnp3  23211  cnpnei  23231  cncls2  23240  cncls  23241  cnntr  23242  cncnp  23247  cndis  23258  paste  23261  cncmp  23359  imacmp  23364  hauscmplem  23373  cnconn  23389  kgencn  23523  xkopt  23622  xkococnlem  23626  fbasrn  23851  fmval  23910  fmf  23912  rnelfmlem  23919  rnelfm  23920  cnflf2  23970  psmetdmdm  24272  xmetres  24331  metres  24332  metcnp  24508  metustsym  24522  cfilucfil  24526  metuel2  24532  iscauf  25249  equivcau  25269  lmclimf  25273  ismbf  25597  ismbfcn  25598  mbfimaicc  25600  mbfimaopn2  25626  ibl0  25756  cniccibl  25810  cnicciblnc  25812  dvnfre  25921  c1liplem1  25965  c1lip2  25967  dvcnvrelem2  25987  plyco0  26159  plyeq0  26178  vieta1lem2  26279  ulm2  26352  ulmss  26364  ulmdvlem2  26368  ulmdvlem3  26369  itgulm  26375  basellem5  27050  nodmon  27616  newbdayim  27897  eedimeq  28969  axcontlem10  29044  wlkn0  29691  wlkres  29739  wlkp1lem1  29742  pthdivtx  29797  cyclnumvtx  29870  dmadjrnb  31979  elnlfn  32001  xppreima  32720  indpreima  32927  symgcom2  33147  tocyc01  33181  tocyccntz  33207  elrspunidl  33490  smatrcl  33942  mdetpmtr1  33969  locfinreflem  33986  hauseqcn  34044  rge0scvg  34095  isrnmeas  34346  omsfval  34440  omscl  34441  omsf  34442  eulerpartlemv  34510  eulerpartlemd  34512  eulerpartlemb  34514  eulerpartlemr  34520  eulerpartlemgvv  34522  eulerpartlemgs2  34526  eulerpartlemn  34527  rpsqrtcn  34739  cvmlift2lem9  35495  cvmlift3lem7  35509  mrsubfval  35692  ivthALT  36519  curf  37921  uncf  37922  unccur  37926  matunitlindflem2  37940  ptrecube  37943  heicant  37978  mbfresfi  37989  itg2addnclem  37994  itg2addnclem2  37995  ftc1anclem1  38016  indexdom  38057  sdclem2  38065  cnres2  38086  sstotbnd2  38097  bnd2lem  38114  ismgmOLD  38173  ismndo2  38197  exidreslem  38200  rngosn3  38247  rngodm1dm2  38255  rhmqusspan  42626  coeq0i  43187  pw2f1ocnv  43467  cnioobibld  43644  dfno2  43857  fresin2  45604  evthiccabs  45928  dvsubcncf  46354  dvmulcncf  46355  dvdivcncf  46357  cnbdibl  46392  fourierdlem48  46584  fourierdlem49  46585  fourierdlem58  46594  fourierdlem59  46595  fourierdlem71  46607  fourierdlem73  46609  fourierdlem74  46610  fourierdlem75  46611  fourierdlem76  46612  fourierdlem80  46616  fourierdlem81  46617  fourierdlem89  46625  fourierdlem91  46627  fourierdlem92  46628  fourierdlem93  46629  fourierdlem94  46630  fourierdlem111  46647  fourierdlem112  46648  fourierdlem113  46649  fouriercn  46662  sge0val  46796  fge0iccico  46800  isomennd  46961  tannpoly  47340  3f1oss1  47525  fafv2elrnb  47685  fmtnoinf  48001  nnsum4primeseven  48278  nnsum4primesevenALTV  48279  upgrimwlklem2  48376  upgrimwlklem3  48377  upgrimtrlslem2  48383  cycl3grtri  48425  domnmsuppn0  48847  scmsuppss  48849  fdivmpt  49018  fdivmptf  49019  refdivmptf  49020  fdivpm  49021  refdivpm  49022  elbigo2  49030  elbigolo1  49035  xpco2  49334