Theorem fdm 6664

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

Syntax hints:   → wi 4   = wceq 1547  dom cdm 5618  ⟶wf 6481

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 208  df-an 397  df-fn 6488  df-f 6489

This theorem is referenced by:  fdmd  6665  fdmi  6666  fimacnv  6677  fssxp  6682  ffdm  6684  f00  6709  f0dom0  6711  f0rn0  6712  fimadmfo  6748  fimadmfoALT  6750  focofo  6752  feldmfvelcdm  7027  dff3  7041  ffvresb  7067  dmfex  7845  fiun  7885  soseq  8099  fsuppeq  8115  fsuppeqg  8116  issmo2  8279  smoiso  8292  mapprc  8767  elpm2r  8782  map0b  8821  mapsnd  8824  brdomg  8895  pw2f1olem  9009  iunmapdisj  9936  fodomfi2  9973  infmap2  10130  coftr  10186  fin23lem40  10264  isf34lem7  10292  axdc3lem2  10364  axdc3lem4  10366  rpnnen1lem4  12921  rpnnen1lem5  12922  fseqsupcl  13930  fseqsupubi  13931  ello12  15469  lo1bdd  15473  elo12  15480  o1bdd  15484  lo1o1  15485  rlimclim  15499  ramval  16970  0ram2  16983  0ramcl  16985  intopsn  18613  mndpsuppss  18724  symgfixf1  19403  f1omvdconj  19412  pmtrdifellem1  19442  pmtrdifellem2  19443  gsumval3  19873  dprdss  19997  dmdprdsplitlem  20005  ablfaclem3  20055  evpmss  21561  pjdm2  21686  islindf2  21789  islindf4  21813  decpmatval  22748  pmatcollpw3lem  22766  iscnp3  23227  cnpnei  23247  cncls2  23256  cncls  23257  cnntr  23258  cncnp  23263  cndis  23274  paste  23277  cncmp  23375  imacmp  23380  hauscmplem  23389  cnconn  23405  kgencn  23539  xkopt  23638  xkococnlem  23642  fbasrn  23867  fmval  23926  fmf  23928  rnelfmlem  23935  rnelfm  23936  cnflf2  23986  psmetdmdm  24288  xmetres  24347  metres  24348  metcnp  24524  metustsym  24538  cfilucfil  24542  metuel2  24548  iscauf  25265  equivcau  25285  lmclimf  25289  ismbf  25613  ismbfcn  25614  mbfimaicc  25616  mbfimaopn2  25642  ibl0  25772  cniccibl  25826  cnicciblnc  25828  dvnfre  25937  c1liplem1  25981  c1lip2  25983  dvcnvrelem2  26003  plyco0  26175  plyeq0  26194  vieta1lem2  26295  ulm2  26368  ulmss  26380  ulmdvlem2  26384  ulmdvlem3  26385  itgulm  26391  basellem5  27066  nodmon  27632  newbdayim  27913  eedimeq  28985  axcontlem10  29060  wlkn0  29707  wlkres  29755  wlkp1lem1  29758  pthdivtx  29813  cyclnumvtx  29886  dmadjrnb  31995  elnlfn  32017  xppreima  32737  indpreima  32944  symgcom2  33165  tocyc01  33199  tocyccntz  33225  elrspunidl  33511  smatrcl  33980  mdetpmtr1  34007  locfinreflem  34024  hauseqcn  34082  rge0scvg  34133  isrnmeas  34384  omsfval  34478  omscl  34479  omsf  34480  eulerpartlemv  34548  eulerpartlemd  34550  eulerpartlemb  34552  eulerpartlemr  34558  eulerpartlemgvv  34560  eulerpartlemgs2  34564  eulerpartlemn  34565  rpsqrtcn  34777  cvmlift2lem9  35539  cvmlift3lem7  35553  mrsubfval  35736  ivthALT  36563  curf  37965  uncf  37966  unccur  37970  matunitlindflem2  37984  ptrecube  37987  heicant  38022  mbfresfi  38033  itg2addnclem  38038  itg2addnclem2  38039  ftc1anclem1  38060  indexdom  38101  sdclem2  38109  cnres2  38130  sstotbnd2  38141  bnd2lem  38158  ismgmOLD  38217  ismndo2  38241  exidreslem  38244  rngosn3  38291  rngodm1dm2  38299  rhmqusspan  42670  coeq0i  43202  pw2f1ocnv  43482  cnioobibld  43659  dfno2  43872  fresin2  45619  evthiccabs  45941  dvsubcncf  46367  dvmulcncf  46368  dvdivcncf  46370  cnbdibl  46405  fourierdlem48  46597  fourierdlem49  46598  fourierdlem58  46607  fourierdlem59  46608  fourierdlem71  46620  fourierdlem73  46622  fourierdlem74  46623  fourierdlem75  46624  fourierdlem76  46625  fourierdlem80  46629  fourierdlem81  46630  fourierdlem89  46638  fourierdlem91  46640  fourierdlem92  46641  fourierdlem93  46642  fourierdlem94  46643  fourierdlem111  46660  fourierdlem112  46661  fourierdlem113  46662  fouriercn  46675  sge0val  46809  fge0iccico  46813  isomennd  46974  tannpoly  47353  3f1oss1  47538  fafv2elrnb  47698  fmtnoinf  48014  nnsum4primeseven  48291  nnsum4primesevenALTV  48292  upgrimwlklem2  48389  upgrimwlklem3  48390  upgrimtrlslem2  48396  cycl3grtri  48438  domnmsuppn0  48860  scmsuppss  48862  fdivmpt  49031  fdivmptf  49032  refdivmptf  49033  fdivpm  49034  refdivpm  49035  elbigo2  49043  elbigolo1  49048  xpco2  49347