Theorem fdm 6299

Description: The domain of a mapping. (Contributed by NM, 2-Aug-1994.)

Assertion

Ref	Expression
fdm	⊢ (𝐹:𝐴⟶𝐵 → dom 𝐹 = 𝐴)

Proof of Theorem fdm

Step	Hyp	Ref	Expression
1		ffn 6291	. 2 ⊢ (𝐹:𝐴⟶𝐵 → 𝐹 Fn 𝐴)
2		fndm 6235	. 2 ⊢ (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴)
3	1, 2	syl 17	1 ⊢ (𝐹:𝐴⟶𝐵 → dom 𝐹 = 𝐴)

Syntax hints:   → wi 4   = wceq 1601  dom cdm 5355   Fn wfn 6130  ⟶wf 6131

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 199  df-an 387  df-fn 6138  df-f 6139

This theorem is referenced by:  fdmd  6300  fdmi  6301  fssxp  6310  ffdm  6312  f00  6337  f0dom0  6339  f0rn0  6340  fimadmfo  6375  fimadmfoALT  6377  foco  6378  fimacnv  6611  dff3  6636  ffvresb  6658  dmfex  7403  frnsuppeq  7588  suppss  7607  issmo2  7729  smoiso  7742  mapprc  8144  elpm2r  8158  map0b  8181  mapsnd  8183  brdomg  8251  pw2f1olem  8352  iunmapdisj  9179  fodomfi2  9216  infmap2  9375  coftr  9430  fin23lem40  9508  isf34lem7  9536  axdc3lem2  9608  axdc3lem4  9610  rpnnen1lem4  12127  rpnnen1lem5  12128  fseqsupcl  13095  fseqsupubi  13096  ello12  14655  lo1bdd  14659  elo12  14666  o1bdd  14670  lo1o1  14671  rlimclim  14685  ramval  16116  0ram2  16129  0ramcl  16131  intopsn  17639  symgfixf1  18240  f1omvdconj  18249  pmtrdifellem1  18279  pmtrdifellem2  18280  gsumval3  18694  dprdss  18815  dmdprdsplitlem  18823  ablfaclem3  18873  evpmss  20327  pjdm2  20454  islindf2  20557  islindf4  20581  decpmatval  20977  pmatcollpw3lem  20995  iscnp3  21456  cnpnei  21476  cncls2  21485  cncls  21486  cnntr  21487  cncnp  21492  cndis  21503  paste  21506  cncmp  21604  imacmp  21609  hauscmplem  21618  cnconn  21634  kgencn  21768  xkopt  21867  xkococnlem  21871  fbasrn  22096  fmval  22155  fmf  22157  rnelfmlem  22164  rnelfm  22165  cnflf2  22215  psmetdmdm  22518  xmetres  22577  metres  22578  metcnp  22754  metustsym  22768  cfilucfil  22772  metuel2  22778  iscauf  23486  equivcau  23506  lmclimf  23510  ismbf  23832  ismbfcn  23833  mbfimaicc  23835  mbfimaopn2  23861  ibl0  23990  cniccibl  24044  dvnfre  24152  c1liplem1  24196  c1lip2  24198  dvcnvrelem2  24218  plyco0  24385  plyeq0  24404  vieta1lem2  24503  ulm2  24576  ulmss  24588  ulmdvlem2  24592  ulmdvlem3  24593  itgulm  24599  basellem5  25263  tgcgr4  25882  eedimeq  26247  axcontlem10  26322  wlkn0  26968  wlkres  27019  wlkresOLD  27021  wlkp1lem1  27024  pthdivtx  27081  dmadjrnb  29337  elnlfn  29359  xppreima  30014  smatrcl  30460  mdetpmtr1  30487  locfinreflem  30505  hauseqcn  30539  rge0scvg  30593  indpreima  30685  isrnmeas  30861  omsfval  30954  omscl  30955  omsf  30956  eulerpartlemv  31024  eulerpartlemd  31026  eulerpartlemb  31028  eulerpartlemr  31034  eulerpartlemgvv  31036  eulerpartlemgs2  31040  eulerpartlemn  31041  rpsqrtcn  31273  cvmlift2lem9  31892  cvmlift3lem7  31906  mrsubfval  32004  soseq  32343  nodmon  32392  ivthALT  32918  curf  34012  uncf  34013  unccur  34017  matunitlindflem2  34032  ptrecube  34035  heicant  34070  mbfresfi  34081  itg2addnclem  34086  itg2addnclem2  34087  cnicciblnc  34106  ftc1anclem1  34110  indexdom  34154  sdclem2  34162  cnres2  34186  sstotbnd2  34197  bnd2lem  34214  ismgmOLD  34273  ismndo2  34297  exidreslem  34300  rngosn3  34347  rngodm1dm2  34355  coeq0i  38276  pw2f1ocnv  38563  cnioobibld  38757  fresin2  40276  evthiccabs  40630  dvsubcncf  41067  dvmulcncf  41068  dvdivcncf  41070  cnbdibl  41105  fourierdlem48  41298  fourierdlem49  41299  fourierdlem58  41308  fourierdlem59  41309  fourierdlem71  41321  fourierdlem73  41323  fourierdlem74  41324  fourierdlem75  41325  fourierdlem76  41326  fourierdlem80  41330  fourierdlem81  41331  fourierdlem89  41339  fourierdlem91  41341  fourierdlem92  41342  fourierdlem93  41343  fourierdlem94  41344  fourierdlem111  41361  fourierdlem112  41362  fourierdlem113  41363  fouriercn  41376  sge0val  41507  fge0iccico  41511  isomennd  41672  fafv2elrnb  42276  fmtnoinf  42469  nnsum4primeseven  42713  nnsum4primesevenALTV  42714  domnmsuppn0  43165  mndpsuppss  43167  scmsuppss  43168  fdivmpt  43349  fdivmptf  43350  refdivmptf  43351  fdivpm  43352  refdivpm  43353  elbigo2  43361  elbigolo1  43366