Theorem fdm 6661

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

Syntax hints:   → wi 4   = wceq 1540  dom cdm 5619  ⟶wf 6478

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 6485  df-f 6486

This theorem is referenced by:  fdmd  6662  fdmi  6663  fimacnv  6674  fssxp  6679  ffdm  6681  f00  6706  f0dom0  6708  f0rn0  6709  fimadmfo  6745  fimadmfoALT  6747  focofo  6749  feldmfvelcdm  7020  dff3  7034  ffvresb  7059  dmfex  7838  fiun  7878  soseq  8092  fsuppeq  8108  fsuppeqg  8109  issmo2  8272  smoiso  8285  mapprc  8757  elpm2r  8772  map0b  8810  mapsnd  8813  brdomg  8884  pw2f1olem  8998  iunmapdisj  9917  fodomfi2  9954  infmap2  10111  coftr  10167  fin23lem40  10245  isf34lem7  10273  axdc3lem2  10345  axdc3lem4  10347  rpnnen1lem4  12881  rpnnen1lem5  12882  fseqsupcl  13884  fseqsupubi  13885  ello12  15423  lo1bdd  15427  elo12  15434  o1bdd  15438  lo1o1  15439  rlimclim  15453  ramval  16920  0ram2  16933  0ramcl  16935  intopsn  18528  mndpsuppss  18639  symgfixf1  19316  f1omvdconj  19325  pmtrdifellem1  19355  pmtrdifellem2  19356  gsumval3  19786  dprdss  19910  dmdprdsplitlem  19918  ablfaclem3  19968  evpmss  21493  pjdm2  21618  islindf2  21721  islindf4  21745  decpmatval  22650  pmatcollpw3lem  22668  iscnp3  23129  cnpnei  23149  cncls2  23158  cncls  23159  cnntr  23160  cncnp  23165  cndis  23176  paste  23179  cncmp  23277  imacmp  23282  hauscmplem  23291  cnconn  23307  kgencn  23441  xkopt  23540  xkococnlem  23544  fbasrn  23769  fmval  23828  fmf  23830  rnelfmlem  23837  rnelfm  23838  cnflf2  23888  psmetdmdm  24191  xmetres  24250  metres  24251  metcnp  24427  metustsym  24441  cfilucfil  24445  metuel2  24451  iscauf  25178  equivcau  25198  lmclimf  25202  ismbf  25527  ismbfcn  25528  mbfimaicc  25530  mbfimaopn2  25556  ibl0  25686  cniccibl  25740  cnicciblnc  25742  dvnfre  25854  c1liplem1  25899  c1lip2  25901  dvcnvrelem2  25921  plyco0  26095  plyeq0  26114  vieta1lem2  26217  ulm2  26292  ulmss  26304  ulmdvlem2  26308  ulmdvlem3  26309  itgulm  26315  basellem5  26993  nodmon  27560  newbdayim  27817  eedimeq  28843  axcontlem10  28918  wlkn0  29566  wlkres  29614  wlkp1lem1  29617  pthdivtx  29672  cyclnumvtx  29745  dmadjrnb  31850  elnlfn  31872  xppreima  32588  indpreima  32808  symgcom2  33026  tocyc01  33060  tocyccntz  33086  elrspunidl  33365  smatrcl  33763  mdetpmtr1  33790  locfinreflem  33807  hauseqcn  33865  rge0scvg  33916  isrnmeas  34167  omsfval  34262  omscl  34263  omsf  34264  eulerpartlemv  34332  eulerpartlemd  34334  eulerpartlemb  34336  eulerpartlemr  34342  eulerpartlemgvv  34344  eulerpartlemgs2  34348  eulerpartlemn  34349  rpsqrtcn  34561  cvmlift2lem9  35284  cvmlift3lem7  35298  mrsubfval  35481  ivthALT  36309  curf  37578  uncf  37579  unccur  37583  matunitlindflem2  37597  ptrecube  37600  heicant  37635  mbfresfi  37646  itg2addnclem  37651  itg2addnclem2  37652  ftc1anclem1  37673  indexdom  37714  sdclem2  37722  cnres2  37743  sstotbnd2  37754  bnd2lem  37771  ismgmOLD  37830  ismndo2  37854  exidreslem  37857  rngosn3  37904  rngodm1dm2  37912  rhmqusspan  42158  coeq0i  42726  pw2f1ocnv  43010  cnioobibld  43187  dfno2  43401  fresin2  45150  evthiccabs  45477  dvsubcncf  45905  dvmulcncf  45906  dvdivcncf  45908  cnbdibl  45943  fourierdlem48  46135  fourierdlem49  46136  fourierdlem58  46145  fourierdlem59  46146  fourierdlem71  46158  fourierdlem73  46160  fourierdlem74  46161  fourierdlem75  46162  fourierdlem76  46163  fourierdlem80  46167  fourierdlem81  46168  fourierdlem89  46176  fourierdlem91  46178  fourierdlem92  46179  fourierdlem93  46180  fourierdlem94  46181  fourierdlem111  46198  fourierdlem112  46199  fourierdlem113  46200  fouriercn  46213  sge0val  46347  fge0iccico  46351  isomennd  46512  tannpoly  46874  3f1oss1  47059  fafv2elrnb  47219  fmtnoinf  47520  nnsum4primeseven  47784  nnsum4primesevenALTV  47785  upgrimwlklem2  47882  upgrimwlklem3  47883  upgrimtrlslem2  47889  cycl3grtri  47931  domnmsuppn0  48353  scmsuppss  48355  fdivmpt  48525  fdivmptf  48526  refdivmptf  48527  fdivpm  48528  refdivpm  48529  elbigo2  48537  elbigolo1  48542  xpco2  48841