Theorem fdm 6700

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

Syntax hints:   → wi 4   = wceq 1540  dom cdm 5641  ⟶wf 6510

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 6517  df-f 6518

This theorem is referenced by:  fdmd  6701  fdmi  6702  fimacnv  6713  fssxp  6718  ffdm  6720  f00  6745  f0dom0  6747  f0rn0  6748  fimadmfo  6784  fimadmfoALT  6786  focofo  6788  feldmfvelcdm  7061  dff3  7075  ffvresb  7100  dmfex  7884  fiun  7924  soseq  8141  fsuppeq  8157  fsuppeqg  8158  issmo2  8321  smoiso  8334  mapprc  8806  elpm2r  8821  map0b  8859  mapsnd  8862  brdomg  8933  pw2f1olem  9050  iunmapdisj  9983  fodomfi2  10020  infmap2  10177  coftr  10233  fin23lem40  10311  isf34lem7  10339  axdc3lem2  10411  axdc3lem4  10413  rpnnen1lem4  12946  rpnnen1lem5  12947  fseqsupcl  13949  fseqsupubi  13950  ello12  15489  lo1bdd  15493  elo12  15500  o1bdd  15504  lo1o1  15505  rlimclim  15519  ramval  16986  0ram2  16999  0ramcl  17001  intopsn  18588  mndpsuppss  18699  symgfixf1  19374  f1omvdconj  19383  pmtrdifellem1  19413  pmtrdifellem2  19414  gsumval3  19844  dprdss  19968  dmdprdsplitlem  19976  ablfaclem3  20026  evpmss  21502  pjdm2  21627  islindf2  21730  islindf4  21754  decpmatval  22659  pmatcollpw3lem  22677  iscnp3  23138  cnpnei  23158  cncls2  23167  cncls  23168  cnntr  23169  cncnp  23174  cndis  23185  paste  23188  cncmp  23286  imacmp  23291  hauscmplem  23300  cnconn  23316  kgencn  23450  xkopt  23549  xkococnlem  23553  fbasrn  23778  fmval  23837  fmf  23839  rnelfmlem  23846  rnelfm  23847  cnflf2  23897  psmetdmdm  24200  xmetres  24259  metres  24260  metcnp  24436  metustsym  24450  cfilucfil  24454  metuel2  24460  iscauf  25187  equivcau  25207  lmclimf  25211  ismbf  25536  ismbfcn  25537  mbfimaicc  25539  mbfimaopn2  25565  ibl0  25695  cniccibl  25749  cnicciblnc  25751  dvnfre  25863  c1liplem1  25908  c1lip2  25910  dvcnvrelem2  25930  plyco0  26104  plyeq0  26123  vieta1lem2  26226  ulm2  26301  ulmss  26313  ulmdvlem2  26317  ulmdvlem3  26318  itgulm  26324  basellem5  27002  nodmon  27569  newbdayim  27821  eedimeq  28832  axcontlem10  28907  wlkn0  29556  wlkres  29605  wlkp1lem1  29608  pthdivtx  29664  cyclnumvtx  29737  dmadjrnb  31842  elnlfn  31864  xppreima  32576  indpreima  32795  symgcom2  33048  tocyc01  33082  tocyccntz  33108  elrspunidl  33406  smatrcl  33793  mdetpmtr1  33820  locfinreflem  33837  hauseqcn  33895  rge0scvg  33946  isrnmeas  34197  omsfval  34292  omscl  34293  omsf  34294  eulerpartlemv  34362  eulerpartlemd  34364  eulerpartlemb  34366  eulerpartlemr  34372  eulerpartlemgvv  34374  eulerpartlemgs2  34378  eulerpartlemn  34379  rpsqrtcn  34591  cvmlift2lem9  35305  cvmlift3lem7  35319  mrsubfval  35502  ivthALT  36330  curf  37599  uncf  37600  unccur  37604  matunitlindflem2  37618  ptrecube  37621  heicant  37656  mbfresfi  37667  itg2addnclem  37672  itg2addnclem2  37673  ftc1anclem1  37694  indexdom  37735  sdclem2  37743  cnres2  37764  sstotbnd2  37775  bnd2lem  37792  ismgmOLD  37851  ismndo2  37875  exidreslem  37878  rngosn3  37925  rngodm1dm2  37933  rhmqusspan  42180  coeq0i  42748  pw2f1ocnv  43033  cnioobibld  43210  dfno2  43424  fresin2  45173  evthiccabs  45501  dvsubcncf  45929  dvmulcncf  45930  dvdivcncf  45932  cnbdibl  45967  fourierdlem48  46159  fourierdlem49  46160  fourierdlem58  46169  fourierdlem59  46170  fourierdlem71  46182  fourierdlem73  46184  fourierdlem74  46185  fourierdlem75  46186  fourierdlem76  46187  fourierdlem80  46191  fourierdlem81  46192  fourierdlem89  46200  fourierdlem91  46202  fourierdlem92  46203  fourierdlem93  46204  fourierdlem94  46205  fourierdlem111  46222  fourierdlem112  46223  fourierdlem113  46224  fouriercn  46237  sge0val  46371  fge0iccico  46375  isomennd  46536  3f1oss1  47080  fafv2elrnb  47240  fmtnoinf  47541  nnsum4primeseven  47805  nnsum4primesevenALTV  47806  upgrimwlklem2  47902  upgrimwlklem3  47903  upgrimtrlslem2  47909  cycl3grtri  47950  domnmsuppn0  48361  scmsuppss  48363  fdivmpt  48533  fdivmptf  48534  refdivmptf  48535  fdivpm  48536  refdivpm  48537  elbigo2  48545  elbigolo1  48550  xpco2  48849