Theorem fdm 6736

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

Syntax hints:   → wi 4   = wceq 1533  dom cdm 5682  ⟶wf 6549

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 206  df-an 395  df-fn 6556  df-f 6557

This theorem is referenced by:  fdmd  6738  fdmi  6739  fimacnv  6750  fssxp  6756  ffdm  6758  f00  6784  f0dom0  6786  f0rn0  6787  fimadmfo  6825  fimadmfoALT  6827  focofo  6829  fimacnvOLD  7085  feldmfvelcdm  7101  dff3  7115  ffvresb  7140  dmfex  7919  fiun  7952  soseq  8170  fsuppeq  8186  fsuppeqg  8187  suppssOLD  8206  issmo2  8376  smoiso  8389  mapprc  8855  elpm2r  8870  map0b  8908  mapsnd  8911  brdomg  8983  brdomgOLD  8984  pw2f1olem  9107  iunmapdisj  10054  fodomfi2  10091  infmap2  10249  coftr  10304  fin23lem40  10382  isf34lem7  10410  axdc3lem2  10482  axdc3lem4  10484  rpnnen1lem4  13002  rpnnen1lem5  13003  fseqsupcl  13982  fseqsupubi  13983  ello12  15500  lo1bdd  15504  elo12  15511  o1bdd  15515  lo1o1  15516  rlimclim  15530  ramval  16984  0ram2  16997  0ramcl  16999  intopsn  18621  symgfixf1  19399  f1omvdconj  19408  pmtrdifellem1  19438  pmtrdifellem2  19439  gsumval3  19869  dprdss  19993  dmdprdsplitlem  20001  ablfaclem3  20051  evpmss  21525  pjdm2  21652  islindf2  21755  islindf4  21779  decpmatval  22687  pmatcollpw3lem  22705  iscnp3  23168  cnpnei  23188  cncls2  23197  cncls  23198  cnntr  23199  cncnp  23204  cndis  23215  paste  23218  cncmp  23316  imacmp  23321  hauscmplem  23330  cnconn  23346  kgencn  23480  xkopt  23579  xkococnlem  23583  fbasrn  23808  fmval  23867  fmf  23869  rnelfmlem  23876  rnelfm  23877  cnflf2  23927  psmetdmdm  24231  xmetres  24290  metres  24291  metcnp  24470  metustsym  24484  cfilucfil  24488  metuel2  24494  iscauf  25228  equivcau  25248  lmclimf  25252  ismbf  25577  ismbfcn  25578  mbfimaicc  25580  mbfimaopn2  25606  ibl0  25736  cniccibl  25790  cnicciblnc  25792  dvnfre  25904  c1liplem1  25949  c1lip2  25951  dvcnvrelem2  25971  plyco0  26146  plyeq0  26165  vieta1lem2  26266  ulm2  26341  ulmss  26353  ulmdvlem2  26357  ulmdvlem3  26358  itgulm  26364  basellem5  27037  nodmon  27603  eedimeq  28729  axcontlem10  28804  wlkn0  29455  wlkres  29504  wlkp1lem1  29507  pthdivtx  29563  dmadjrnb  31736  elnlfn  31758  xppreima  32453  symgcom2  32828  tocyc01  32860  tocyccntz  32886  elrspunidl  33169  smatrcl  33430  mdetpmtr1  33457  locfinreflem  33474  hauseqcn  33532  rge0scvg  33583  indpreima  33677  isrnmeas  33852  omsfval  33947  omscl  33948  omsf  33949  eulerpartlemv  34017  eulerpartlemd  34019  eulerpartlemb  34021  eulerpartlemr  34027  eulerpartlemgvv  34029  eulerpartlemgs2  34033  eulerpartlemn  34034  rpsqrtcn  34258  cvmlift2lem9  34954  cvmlift3lem7  34968  mrsubfval  35151  ivthALT  35852  curf  37104  uncf  37105  unccur  37109  matunitlindflem2  37123  ptrecube  37126  heicant  37161  mbfresfi  37172  itg2addnclem  37177  itg2addnclem2  37178  ftc1anclem1  37199  indexdom  37240  sdclem2  37248  cnres2  37269  sstotbnd2  37280  bnd2lem  37297  ismgmOLD  37356  ismndo2  37380  exidreslem  37383  rngosn3  37430  rngodm1dm2  37438  coeq0i  42204  pw2f1ocnv  42489  cnioobibld  42673  dfno2  42889  fresin2  44575  evthiccabs  44910  dvsubcncf  45341  dvmulcncf  45342  dvdivcncf  45344  cnbdibl  45379  fourierdlem48  45571  fourierdlem49  45572  fourierdlem58  45581  fourierdlem59  45582  fourierdlem71  45594  fourierdlem73  45596  fourierdlem74  45597  fourierdlem75  45598  fourierdlem76  45599  fourierdlem80  45603  fourierdlem81  45604  fourierdlem89  45612  fourierdlem91  45614  fourierdlem92  45615  fourierdlem93  45616  fourierdlem94  45617  fourierdlem111  45634  fourierdlem112  45635  fourierdlem113  45636  fouriercn  45649  sge0val  45783  fge0iccico  45787  isomennd  45948  fafv2elrnb  46644  fmtnoinf  46905  nnsum4primeseven  47169  nnsum4primesevenALTV  47170  domnmsuppn0  47511  mndpsuppss  47513  scmsuppss  47514  fdivmpt  47691  fdivmptf  47692  refdivmptf  47693  fdivpm  47694  refdivpm  47695  elbigo2  47703  elbigolo1  47708