Theorem fdm 6677

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

Syntax hints:   → wi 4   = wceq 1542  dom cdm 5631  ⟶wf 6494

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 6501  df-f 6502

This theorem is referenced by:  fdmd  6678  fdmi  6679  fimacnv  6690  fssxp  6695  ffdm  6697  f00  6722  f0dom0  6724  f0rn0  6725  fimadmfo  6761  fimadmfoALT  6763  focofo  6765  feldmfvelcdm  7038  dff3  7052  ffvresb  7078  dmfex  7856  fiun  7896  soseq  8109  fsuppeq  8125  fsuppeqg  8126  issmo2  8289  smoiso  8302  mapprc  8777  elpm2r  8792  map0b  8831  mapsnd  8834  brdomg  8905  pw2f1olem  9019  iunmapdisj  9945  fodomfi2  9982  infmap2  10139  coftr  10195  fin23lem40  10273  isf34lem7  10301  axdc3lem2  10373  axdc3lem4  10375  rpnnen1lem4  12930  rpnnen1lem5  12931  fseqsupcl  13939  fseqsupubi  13940  ello12  15478  lo1bdd  15482  elo12  15489  o1bdd  15493  lo1o1  15494  rlimclim  15508  ramval  16979  0ram2  16992  0ramcl  16994  intopsn  18622  mndpsuppss  18733  symgfixf1  19412  f1omvdconj  19421  pmtrdifellem1  19451  pmtrdifellem2  19452  gsumval3  19882  dprdss  20006  dmdprdsplitlem  20014  ablfaclem3  20064  evpmss  21566  pjdm2  21691  islindf2  21794  islindf4  21818  decpmatval  22730  pmatcollpw3lem  22748  iscnp3  23209  cnpnei  23229  cncls2  23238  cncls  23239  cnntr  23240  cncnp  23245  cndis  23256  paste  23259  cncmp  23357  imacmp  23362  hauscmplem  23371  cnconn  23387  kgencn  23521  xkopt  23620  xkococnlem  23624  fbasrn  23849  fmval  23908  fmf  23910  rnelfmlem  23917  rnelfm  23918  cnflf2  23968  psmetdmdm  24270  xmetres  24329  metres  24330  metcnp  24506  metustsym  24520  cfilucfil  24524  metuel2  24530  iscauf  25247  equivcau  25267  lmclimf  25271  ismbf  25595  ismbfcn  25596  mbfimaicc  25598  mbfimaopn2  25624  ibl0  25754  cniccibl  25808  cnicciblnc  25810  dvnfre  25919  c1liplem1  25963  c1lip2  25965  dvcnvrelem2  25985  plyco0  26157  plyeq0  26176  vieta1lem2  26277  ulm2  26350  ulmss  26362  ulmdvlem2  26366  ulmdvlem3  26367  itgulm  26373  basellem5  27048  nodmon  27614  newbdayim  27895  eedimeq  28967  axcontlem10  29042  wlkn0  29689  wlkres  29737  wlkp1lem1  29740  pthdivtx  29795  cyclnumvtx  29868  dmadjrnb  31977  elnlfn  31999  xppreima  32718  indpreima  32925  symgcom2  33145  tocyc01  33179  tocyccntz  33205  elrspunidl  33488  smatrcl  33940  mdetpmtr1  33967  locfinreflem  33984  hauseqcn  34042  rge0scvg  34093  isrnmeas  34344  omsfval  34438  omscl  34439  omsf  34440  eulerpartlemv  34508  eulerpartlemd  34510  eulerpartlemb  34512  eulerpartlemr  34518  eulerpartlemgvv  34520  eulerpartlemgs2  34524  eulerpartlemn  34525  rpsqrtcn  34737  cvmlift2lem9  35493  cvmlift3lem7  35507  mrsubfval  35690  ivthALT  36517  curf  37919  uncf  37920  unccur  37924  matunitlindflem2  37938  ptrecube  37941  heicant  37976  mbfresfi  37987  itg2addnclem  37992  itg2addnclem2  37993  ftc1anclem1  38014  indexdom  38055  sdclem2  38063  cnres2  38084  sstotbnd2  38095  bnd2lem  38112  ismgmOLD  38171  ismndo2  38195  exidreslem  38198  rngosn3  38245  rngodm1dm2  38253  rhmqusspan  42624  coeq0i  43185  pw2f1ocnv  43465  cnioobibld  43642  dfno2  43855  fresin2  45602  evthiccabs  45926  dvsubcncf  46352  dvmulcncf  46353  dvdivcncf  46355  cnbdibl  46390  fourierdlem48  46582  fourierdlem49  46583  fourierdlem58  46592  fourierdlem59  46593  fourierdlem71  46605  fourierdlem73  46607  fourierdlem74  46608  fourierdlem75  46609  fourierdlem76  46610  fourierdlem80  46614  fourierdlem81  46615  fourierdlem89  46623  fourierdlem91  46625  fourierdlem92  46626  fourierdlem93  46627  fourierdlem94  46628  fourierdlem111  46645  fourierdlem112  46646  fourierdlem113  46647  fouriercn  46660  sge0val  46794  fge0iccico  46798  isomennd  46959  tannpoly  47338  3f1oss1  47523  fafv2elrnb  47683  fmtnoinf  47999  nnsum4primeseven  48276  nnsum4primesevenALTV  48277  upgrimwlklem2  48374  upgrimwlklem3  48375  upgrimtrlslem2  48381  cycl3grtri  48423  domnmsuppn0  48845  scmsuppss  48847  fdivmpt  49016  fdivmptf  49017  refdivmptf  49018  fdivpm  49019  refdivpm  49020  elbigo2  49028  elbigolo1  49033  xpco2  49332