Theorem fdm 6727

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

Syntax hints:   → wi 4   = wceq 1542  dom cdm 5677  ⟶wf 6540

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 398  df-fn 6547  df-f 6548

This theorem is referenced by:  fdmd  6729  fdmi  6730  fimacnv  6740  fssxp  6746  ffdm  6748  f00  6774  f0dom0  6776  f0rn0  6777  fimadmfo  6815  fimadmfoALT  6817  focofo  6819  fimacnvOLD  7073  dff3  7102  ffvresb  7124  dmfex  7898  fiun  7929  soseq  8145  fsuppeq  8160  fsuppeqg  8161  suppssOLD  8180  issmo2  8349  smoiso  8362  mapprc  8824  elpm2r  8839  map0b  8877  mapsnd  8880  brdomg  8952  brdomgOLD  8953  pw2f1olem  9076  iunmapdisj  10018  fodomfi2  10055  infmap2  10213  coftr  10268  fin23lem40  10346  isf34lem7  10374  axdc3lem2  10446  axdc3lem4  10448  rpnnen1lem4  12964  rpnnen1lem5  12965  fseqsupcl  13942  fseqsupubi  13943  ello12  15460  lo1bdd  15464  elo12  15471  o1bdd  15475  lo1o1  15476  rlimclim  15490  ramval  16941  0ram2  16954  0ramcl  16956  intopsn  18573  symgfixf1  19305  f1omvdconj  19314  pmtrdifellem1  19344  pmtrdifellem2  19345  gsumval3  19775  dprdss  19899  dmdprdsplitlem  19907  ablfaclem3  19957  evpmss  21139  pjdm2  21266  islindf2  21369  islindf4  21393  decpmatval  22267  pmatcollpw3lem  22285  iscnp3  22748  cnpnei  22768  cncls2  22777  cncls  22778  cnntr  22779  cncnp  22784  cndis  22795  paste  22798  cncmp  22896  imacmp  22901  hauscmplem  22910  cnconn  22926  kgencn  23060  xkopt  23159  xkococnlem  23163  fbasrn  23388  fmval  23447  fmf  23449  rnelfmlem  23456  rnelfm  23457  cnflf2  23507  psmetdmdm  23811  xmetres  23870  metres  23871  metcnp  24050  metustsym  24064  cfilucfil  24068  metuel2  24074  iscauf  24797  equivcau  24817  lmclimf  24821  ismbf  25145  ismbfcn  25146  mbfimaicc  25148  mbfimaopn2  25174  ibl0  25304  cniccibl  25358  cnicciblnc  25360  dvnfre  25469  c1liplem1  25513  c1lip2  25515  dvcnvrelem2  25535  plyco0  25706  plyeq0  25725  vieta1lem2  25824  ulm2  25897  ulmss  25909  ulmdvlem2  25913  ulmdvlem3  25914  itgulm  25920  basellem5  26589  nodmon  27153  eedimeq  28156  axcontlem10  28231  wlkn0  28878  wlkres  28927  wlkp1lem1  28930  pthdivtx  28986  dmadjrnb  31159  elnlfn  31181  xppreima  31871  symgcom2  32245  tocyc01  32277  tocyccntz  32303  elrspunidl  32546  smatrcl  32776  mdetpmtr1  32803  locfinreflem  32820  hauseqcn  32878  rge0scvg  32929  indpreima  33023  isrnmeas  33198  omsfval  33293  omscl  33294  omsf  33295  eulerpartlemv  33363  eulerpartlemd  33365  eulerpartlemb  33367  eulerpartlemr  33373  eulerpartlemgvv  33375  eulerpartlemgs2  33379  eulerpartlemn  33380  rpsqrtcn  33605  cvmlift2lem9  34302  cvmlift3lem7  34316  mrsubfval  34499  ivthALT  35220  curf  36466  uncf  36467  unccur  36471  matunitlindflem2  36485  ptrecube  36488  heicant  36523  mbfresfi  36534  itg2addnclem  36539  itg2addnclem2  36540  ftc1anclem1  36561  indexdom  36602  sdclem2  36610  cnres2  36631  sstotbnd2  36642  bnd2lem  36659  ismgmOLD  36718  ismndo2  36742  exidreslem  36745  rngosn3  36792  rngodm1dm2  36800  coeq0i  41491  pw2f1ocnv  41776  cnioobibld  41963  dfno2  42179  fresin2  43868  evthiccabs  44209  dvsubcncf  44640  dvmulcncf  44641  dvdivcncf  44643  cnbdibl  44678  fourierdlem48  44870  fourierdlem49  44871  fourierdlem58  44880  fourierdlem59  44881  fourierdlem71  44893  fourierdlem73  44895  fourierdlem74  44896  fourierdlem75  44897  fourierdlem76  44898  fourierdlem80  44902  fourierdlem81  44903  fourierdlem89  44911  fourierdlem91  44913  fourierdlem92  44914  fourierdlem93  44915  fourierdlem94  44916  fourierdlem111  44933  fourierdlem112  44934  fourierdlem113  44935  fouriercn  44948  sge0val  45082  fge0iccico  45086  isomennd  45247  fafv2elrnb  45943  fmtnoinf  46204  nnsum4primeseven  46468  nnsum4primesevenALTV  46469  domnmsuppn0  47045  mndpsuppss  47047  scmsuppss  47048  fdivmpt  47226  fdivmptf  47227  refdivmptf  47228  fdivpm  47229  refdivpm  47230  elbigo2  47238  elbigolo1  47243