Theorem fdm 6669

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

Syntax hints:   → wi 4   = wceq 1541  dom cdm 5622  ⟶wf 6486

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 6493  df-f 6494

This theorem is referenced by:  fdmd  6670  fdmi  6671  fimacnv  6682  fssxp  6687  ffdm  6689  f00  6714  f0dom0  6716  f0rn0  6717  fimadmfo  6753  fimadmfoALT  6755  focofo  6757  feldmfvelcdm  7029  dff3  7043  ffvresb  7068  dmfex  7845  fiun  7885  soseq  8099  fsuppeq  8115  fsuppeqg  8116  issmo2  8279  smoiso  8292  mapprc  8765  elpm2r  8780  map0b  8819  mapsnd  8822  brdomg  8893  pw2f1olem  9007  iunmapdisj  9931  fodomfi2  9968  infmap2  10125  coftr  10181  fin23lem40  10259  isf34lem7  10287  axdc3lem2  10359  axdc3lem4  10361  rpnnen1lem4  12891  rpnnen1lem5  12892  fseqsupcl  13898  fseqsupubi  13899  ello12  15437  lo1bdd  15441  elo12  15448  o1bdd  15452  lo1o1  15453  rlimclim  15467  ramval  16934  0ram2  16947  0ramcl  16949  intopsn  18577  mndpsuppss  18688  symgfixf1  19364  f1omvdconj  19373  pmtrdifellem1  19403  pmtrdifellem2  19404  gsumval3  19834  dprdss  19958  dmdprdsplitlem  19966  ablfaclem3  20016  evpmss  21539  pjdm2  21664  islindf2  21767  islindf4  21791  decpmatval  22707  pmatcollpw3lem  22725  iscnp3  23186  cnpnei  23206  cncls2  23215  cncls  23216  cnntr  23217  cncnp  23222  cndis  23233  paste  23236  cncmp  23334  imacmp  23339  hauscmplem  23348  cnconn  23364  kgencn  23498  xkopt  23597  xkococnlem  23601  fbasrn  23826  fmval  23885  fmf  23887  rnelfmlem  23894  rnelfm  23895  cnflf2  23945  psmetdmdm  24247  xmetres  24306  metres  24307  metcnp  24483  metustsym  24497  cfilucfil  24501  metuel2  24507  iscauf  25234  equivcau  25254  lmclimf  25258  ismbf  25583  ismbfcn  25584  mbfimaicc  25586  mbfimaopn2  25612  ibl0  25742  cniccibl  25796  cnicciblnc  25798  dvnfre  25910  c1liplem1  25955  c1lip2  25957  dvcnvrelem2  25977  plyco0  26151  plyeq0  26170  vieta1lem2  26273  ulm2  26348  ulmss  26360  ulmdvlem2  26364  ulmdvlem3  26365  itgulm  26371  basellem5  27049  nodmon  27616  newbdayim  27875  eedimeq  28920  axcontlem10  28995  wlkn0  29643  wlkres  29691  wlkp1lem1  29694  pthdivtx  29749  cyclnumvtx  29822  dmadjrnb  31930  elnlfn  31952  xppreima  32672  indpreima  32896  symgcom2  33115  tocyc01  33149  tocyccntz  33175  elrspunidl  33458  smatrcl  33902  mdetpmtr1  33929  locfinreflem  33946  hauseqcn  34004  rge0scvg  34055  isrnmeas  34306  omsfval  34400  omscl  34401  omsf  34402  eulerpartlemv  34470  eulerpartlemd  34472  eulerpartlemb  34474  eulerpartlemr  34480  eulerpartlemgvv  34482  eulerpartlemgs2  34486  eulerpartlemn  34487  rpsqrtcn  34699  cvmlift2lem9  35454  cvmlift3lem7  35468  mrsubfval  35651  ivthALT  36478  curf  37738  uncf  37739  unccur  37743  matunitlindflem2  37757  ptrecube  37760  heicant  37795  mbfresfi  37806  itg2addnclem  37811  itg2addnclem2  37812  ftc1anclem1  37833  indexdom  37874  sdclem2  37882  cnres2  37903  sstotbnd2  37914  bnd2lem  37931  ismgmOLD  37990  ismndo2  38014  exidreslem  38017  rngosn3  38064  rngodm1dm2  38072  rhmqusspan  42378  coeq0i  42937  pw2f1ocnv  43221  cnioobibld  43398  dfno2  43611  fresin2  45358  evthiccabs  45684  dvsubcncf  46110  dvmulcncf  46111  dvdivcncf  46113  cnbdibl  46148  fourierdlem48  46340  fourierdlem49  46341  fourierdlem58  46350  fourierdlem59  46351  fourierdlem71  46363  fourierdlem73  46365  fourierdlem74  46366  fourierdlem75  46367  fourierdlem76  46368  fourierdlem80  46372  fourierdlem81  46373  fourierdlem89  46381  fourierdlem91  46383  fourierdlem92  46384  fourierdlem93  46385  fourierdlem94  46386  fourierdlem111  46403  fourierdlem112  46404  fourierdlem113  46405  fouriercn  46418  sge0val  46552  fge0iccico  46556  isomennd  46717  tannpoly  47078  3f1oss1  47263  fafv2elrnb  47423  fmtnoinf  47724  nnsum4primeseven  47988  nnsum4primesevenALTV  47989  upgrimwlklem2  48086  upgrimwlklem3  48087  upgrimtrlslem2  48093  cycl3grtri  48135  domnmsuppn0  48557  scmsuppss  48559  fdivmpt  48728  fdivmptf  48729  refdivmptf  48730  fdivpm  48731  refdivpm  48732  elbigo2  48740  elbigolo1  48745  xpco2  49044