Theorem fdm 6679

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

Syntax hints:   → wi 4   = wceq 1542  dom cdm 5632  ⟶wf 6496

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 6503  df-f 6504

This theorem is referenced by:  fdmd  6680  fdmi  6681  fimacnv  6692  fssxp  6697  ffdm  6699  f00  6724  f0dom0  6726  f0rn0  6727  fimadmfo  6763  fimadmfoALT  6765  focofo  6767  feldmfvelcdm  7040  dff3  7054  ffvresb  7080  dmfex  7857  fiun  7897  soseq  8111  fsuppeq  8127  fsuppeqg  8128  issmo2  8291  smoiso  8304  mapprc  8779  elpm2r  8794  map0b  8833  mapsnd  8836  brdomg  8907  pw2f1olem  9021  iunmapdisj  9945  fodomfi2  9982  infmap2  10139  coftr  10195  fin23lem40  10273  isf34lem7  10301  axdc3lem2  10373  axdc3lem4  10375  rpnnen1lem4  12905  rpnnen1lem5  12906  fseqsupcl  13912  fseqsupubi  13913  ello12  15451  lo1bdd  15455  elo12  15462  o1bdd  15466  lo1o1  15467  rlimclim  15481  ramval  16948  0ram2  16961  0ramcl  16963  intopsn  18591  mndpsuppss  18702  symgfixf1  19378  f1omvdconj  19387  pmtrdifellem1  19417  pmtrdifellem2  19418  gsumval3  19848  dprdss  19972  dmdprdsplitlem  19980  ablfaclem3  20030  evpmss  21553  pjdm2  21678  islindf2  21781  islindf4  21805  decpmatval  22721  pmatcollpw3lem  22739  iscnp3  23200  cnpnei  23220  cncls2  23229  cncls  23230  cnntr  23231  cncnp  23236  cndis  23247  paste  23250  cncmp  23348  imacmp  23353  hauscmplem  23362  cnconn  23378  kgencn  23512  xkopt  23611  xkococnlem  23615  fbasrn  23840  fmval  23899  fmf  23901  rnelfmlem  23908  rnelfm  23909  cnflf2  23959  psmetdmdm  24261  xmetres  24320  metres  24321  metcnp  24497  metustsym  24511  cfilucfil  24515  metuel2  24521  iscauf  25248  equivcau  25268  lmclimf  25272  ismbf  25597  ismbfcn  25598  mbfimaicc  25600  mbfimaopn2  25626  ibl0  25756  cniccibl  25810  cnicciblnc  25812  dvnfre  25924  c1liplem1  25969  c1lip2  25971  dvcnvrelem2  25991  plyco0  26165  plyeq0  26184  vieta1lem2  26287  ulm2  26362  ulmss  26374  ulmdvlem2  26378  ulmdvlem3  26379  itgulm  26385  basellem5  27063  nodmon  27630  newbdayim  27911  eedimeq  28983  axcontlem10  29058  wlkn0  29706  wlkres  29754  wlkp1lem1  29757  pthdivtx  29812  cyclnumvtx  29885  dmadjrnb  31994  elnlfn  32016  xppreima  32735  indpreima  32958  symgcom2  33178  tocyc01  33212  tocyccntz  33238  elrspunidl  33521  smatrcl  33974  mdetpmtr1  34001  locfinreflem  34018  hauseqcn  34076  rge0scvg  34127  isrnmeas  34378  omsfval  34472  omscl  34473  omsf  34474  eulerpartlemv  34542  eulerpartlemd  34544  eulerpartlemb  34546  eulerpartlemr  34552  eulerpartlemgvv  34554  eulerpartlemgs2  34558  eulerpartlemn  34559  rpsqrtcn  34771  cvmlift2lem9  35527  cvmlift3lem7  35541  mrsubfval  35724  ivthALT  36551  curf  37849  uncf  37850  unccur  37854  matunitlindflem2  37868  ptrecube  37871  heicant  37906  mbfresfi  37917  itg2addnclem  37922  itg2addnclem2  37923  ftc1anclem1  37944  indexdom  37985  sdclem2  37993  cnres2  38014  sstotbnd2  38025  bnd2lem  38042  ismgmOLD  38101  ismndo2  38125  exidreslem  38128  rngosn3  38175  rngodm1dm2  38183  rhmqusspan  42555  coeq0i  43110  pw2f1ocnv  43394  cnioobibld  43571  dfno2  43784  fresin2  45531  evthiccabs  45856  dvsubcncf  46282  dvmulcncf  46283  dvdivcncf  46285  cnbdibl  46320  fourierdlem48  46512  fourierdlem49  46513  fourierdlem58  46522  fourierdlem59  46523  fourierdlem71  46535  fourierdlem73  46537  fourierdlem74  46538  fourierdlem75  46539  fourierdlem76  46540  fourierdlem80  46544  fourierdlem81  46545  fourierdlem89  46553  fourierdlem91  46555  fourierdlem92  46556  fourierdlem93  46557  fourierdlem94  46558  fourierdlem111  46575  fourierdlem112  46576  fourierdlem113  46577  fouriercn  46590  sge0val  46724  fge0iccico  46728  isomennd  46889  tannpoly  47250  3f1oss1  47435  fafv2elrnb  47595  fmtnoinf  47896  nnsum4primeseven  48160  nnsum4primesevenALTV  48161  upgrimwlklem2  48258  upgrimwlklem3  48259  upgrimtrlslem2  48265  cycl3grtri  48307  domnmsuppn0  48729  scmsuppss  48731  fdivmpt  48900  fdivmptf  48901  refdivmptf  48902  fdivpm  48903  refdivpm  48904  elbigo2  48912  elbigolo1  48917  xpco2  49216