Theorem fdm 6697

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

Syntax hints:   → wi 4   = wceq 1540  dom cdm 5638  ⟶wf 6507

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 6514  df-f 6515

This theorem is referenced by:  fdmd  6698  fdmi  6699  fimacnv  6710  fssxp  6715  ffdm  6717  f00  6742  f0dom0  6744  f0rn0  6745  fimadmfo  6781  fimadmfoALT  6783  focofo  6785  feldmfvelcdm  7058  dff3  7072  ffvresb  7097  dmfex  7881  fiun  7921  soseq  8138  fsuppeq  8154  fsuppeqg  8155  issmo2  8318  smoiso  8331  mapprc  8803  elpm2r  8818  map0b  8856  mapsnd  8859  brdomg  8930  pw2f1olem  9045  iunmapdisj  9976  fodomfi2  10013  infmap2  10170  coftr  10226  fin23lem40  10304  isf34lem7  10332  axdc3lem2  10404  axdc3lem4  10406  rpnnen1lem4  12939  rpnnen1lem5  12940  fseqsupcl  13942  fseqsupubi  13943  ello12  15482  lo1bdd  15486  elo12  15493  o1bdd  15497  lo1o1  15498  rlimclim  15512  ramval  16979  0ram2  16992  0ramcl  16994  intopsn  18581  mndpsuppss  18692  symgfixf1  19367  f1omvdconj  19376  pmtrdifellem1  19406  pmtrdifellem2  19407  gsumval3  19837  dprdss  19961  dmdprdsplitlem  19969  ablfaclem3  20019  evpmss  21495  pjdm2  21620  islindf2  21723  islindf4  21747  decpmatval  22652  pmatcollpw3lem  22670  iscnp3  23131  cnpnei  23151  cncls2  23160  cncls  23161  cnntr  23162  cncnp  23167  cndis  23178  paste  23181  cncmp  23279  imacmp  23284  hauscmplem  23293  cnconn  23309  kgencn  23443  xkopt  23542  xkococnlem  23546  fbasrn  23771  fmval  23830  fmf  23832  rnelfmlem  23839  rnelfm  23840  cnflf2  23890  psmetdmdm  24193  xmetres  24252  metres  24253  metcnp  24429  metustsym  24443  cfilucfil  24447  metuel2  24453  iscauf  25180  equivcau  25200  lmclimf  25204  ismbf  25529  ismbfcn  25530  mbfimaicc  25532  mbfimaopn2  25558  ibl0  25688  cniccibl  25742  cnicciblnc  25744  dvnfre  25856  c1liplem1  25901  c1lip2  25903  dvcnvrelem2  25923  plyco0  26097  plyeq0  26116  vieta1lem2  26219  ulm2  26294  ulmss  26306  ulmdvlem2  26310  ulmdvlem3  26311  itgulm  26317  basellem5  26995  nodmon  27562  newbdayim  27814  eedimeq  28825  axcontlem10  28900  wlkn0  29549  wlkres  29598  wlkp1lem1  29601  pthdivtx  29657  cyclnumvtx  29730  dmadjrnb  31835  elnlfn  31857  xppreima  32569  indpreima  32788  symgcom2  33041  tocyc01  33075  tocyccntz  33101  elrspunidl  33399  smatrcl  33786  mdetpmtr1  33813  locfinreflem  33830  hauseqcn  33888  rge0scvg  33939  isrnmeas  34190  omsfval  34285  omscl  34286  omsf  34287  eulerpartlemv  34355  eulerpartlemd  34357  eulerpartlemb  34359  eulerpartlemr  34365  eulerpartlemgvv  34367  eulerpartlemgs2  34371  eulerpartlemn  34372  rpsqrtcn  34584  cvmlift2lem9  35298  cvmlift3lem7  35312  mrsubfval  35495  ivthALT  36323  curf  37592  uncf  37593  unccur  37597  matunitlindflem2  37611  ptrecube  37614  heicant  37649  mbfresfi  37660  itg2addnclem  37665  itg2addnclem2  37666  ftc1anclem1  37687  indexdom  37728  sdclem2  37736  cnres2  37757  sstotbnd2  37768  bnd2lem  37785  ismgmOLD  37844  ismndo2  37868  exidreslem  37871  rngosn3  37918  rngodm1dm2  37926  rhmqusspan  42173  coeq0i  42741  pw2f1ocnv  43026  cnioobibld  43203  dfno2  43417  fresin2  45166  evthiccabs  45494  dvsubcncf  45922  dvmulcncf  45923  dvdivcncf  45925  cnbdibl  45960  fourierdlem48  46152  fourierdlem49  46153  fourierdlem58  46162  fourierdlem59  46163  fourierdlem71  46175  fourierdlem73  46177  fourierdlem74  46178  fourierdlem75  46179  fourierdlem76  46180  fourierdlem80  46184  fourierdlem81  46185  fourierdlem89  46193  fourierdlem91  46195  fourierdlem92  46196  fourierdlem93  46197  fourierdlem94  46198  fourierdlem111  46215  fourierdlem112  46216  fourierdlem113  46217  fouriercn  46230  sge0val  46364  fge0iccico  46368  isomennd  46529  tannpoly  46891  3f1oss1  47076  fafv2elrnb  47236  fmtnoinf  47537  nnsum4primeseven  47801  nnsum4primesevenALTV  47802  upgrimwlklem2  47898  upgrimwlklem3  47899  upgrimtrlslem2  47905  cycl3grtri  47946  domnmsuppn0  48357  scmsuppss  48359  fdivmpt  48529  fdivmptf  48530  refdivmptf  48531  fdivpm  48532  refdivpm  48533  elbigo2  48541  elbigolo1  48546  xpco2  48845