Theorem fdm 6715

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

Syntax hints:   → wi 4   = wceq 1540  dom cdm 5654  ⟶wf 6527

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 6534  df-f 6535

This theorem is referenced by:  fdmd  6716  fdmi  6717  fimacnv  6728  fssxp  6733  ffdm  6735  f00  6760  f0dom0  6762  f0rn0  6763  fimadmfo  6799  fimadmfoALT  6801  focofo  6803  feldmfvelcdm  7076  dff3  7090  ffvresb  7115  dmfex  7901  fiun  7941  soseq  8158  fsuppeq  8174  fsuppeqg  8175  issmo2  8363  smoiso  8376  mapprc  8844  elpm2r  8859  map0b  8897  mapsnd  8900  brdomg  8971  brdomgOLD  8972  pw2f1olem  9090  iunmapdisj  10037  fodomfi2  10074  infmap2  10231  coftr  10287  fin23lem40  10365  isf34lem7  10393  axdc3lem2  10465  axdc3lem4  10467  rpnnen1lem4  12996  rpnnen1lem5  12997  fseqsupcl  13995  fseqsupubi  13996  ello12  15532  lo1bdd  15536  elo12  15543  o1bdd  15547  lo1o1  15548  rlimclim  15562  ramval  17028  0ram2  17041  0ramcl  17043  intopsn  18632  mndpsuppss  18743  symgfixf1  19418  f1omvdconj  19427  pmtrdifellem1  19457  pmtrdifellem2  19458  gsumval3  19888  dprdss  20012  dmdprdsplitlem  20020  ablfaclem3  20070  evpmss  21546  pjdm2  21671  islindf2  21774  islindf4  21798  decpmatval  22703  pmatcollpw3lem  22721  iscnp3  23182  cnpnei  23202  cncls2  23211  cncls  23212  cnntr  23213  cncnp  23218  cndis  23229  paste  23232  cncmp  23330  imacmp  23335  hauscmplem  23344  cnconn  23360  kgencn  23494  xkopt  23593  xkococnlem  23597  fbasrn  23822  fmval  23881  fmf  23883  rnelfmlem  23890  rnelfm  23891  cnflf2  23941  psmetdmdm  24244  xmetres  24303  metres  24304  metcnp  24480  metustsym  24494  cfilucfil  24498  metuel2  24504  iscauf  25232  equivcau  25252  lmclimf  25256  ismbf  25581  ismbfcn  25582  mbfimaicc  25584  mbfimaopn2  25610  ibl0  25740  cniccibl  25794  cnicciblnc  25796  dvnfre  25908  c1liplem1  25953  c1lip2  25955  dvcnvrelem2  25975  plyco0  26149  plyeq0  26168  vieta1lem2  26271  ulm2  26346  ulmss  26358  ulmdvlem2  26362  ulmdvlem3  26363  itgulm  26369  basellem5  27047  nodmon  27614  newbdayim  27866  eedimeq  28877  axcontlem10  28952  wlkn0  29601  wlkres  29650  wlkp1lem1  29653  pthdivtx  29709  cyclnumvtx  29782  dmadjrnb  31887  elnlfn  31909  xppreima  32623  indpreima  32842  symgcom2  33095  tocyc01  33129  tocyccntz  33155  elrspunidl  33443  smatrcl  33827  mdetpmtr1  33854  locfinreflem  33871  hauseqcn  33929  rge0scvg  33980  isrnmeas  34231  omsfval  34326  omscl  34327  omsf  34328  eulerpartlemv  34396  eulerpartlemd  34398  eulerpartlemb  34400  eulerpartlemr  34406  eulerpartlemgvv  34408  eulerpartlemgs2  34412  eulerpartlemn  34413  rpsqrtcn  34625  cvmlift2lem9  35333  cvmlift3lem7  35347  mrsubfval  35530  ivthALT  36353  curf  37622  uncf  37623  unccur  37627  matunitlindflem2  37641  ptrecube  37644  heicant  37679  mbfresfi  37690  itg2addnclem  37695  itg2addnclem2  37696  ftc1anclem1  37717  indexdom  37758  sdclem2  37766  cnres2  37787  sstotbnd2  37798  bnd2lem  37815  ismgmOLD  37874  ismndo2  37898  exidreslem  37901  rngosn3  37948  rngodm1dm2  37956  rhmqusspan  42198  coeq0i  42776  pw2f1ocnv  43061  cnioobibld  43238  dfno2  43452  fresin2  45196  evthiccabs  45525  dvsubcncf  45953  dvmulcncf  45954  dvdivcncf  45956  cnbdibl  45991  fourierdlem48  46183  fourierdlem49  46184  fourierdlem58  46193  fourierdlem59  46194  fourierdlem71  46206  fourierdlem73  46208  fourierdlem74  46209  fourierdlem75  46210  fourierdlem76  46211  fourierdlem80  46215  fourierdlem81  46216  fourierdlem89  46224  fourierdlem91  46226  fourierdlem92  46227  fourierdlem93  46228  fourierdlem94  46229  fourierdlem111  46246  fourierdlem112  46247  fourierdlem113  46248  fouriercn  46261  sge0val  46395  fge0iccico  46399  isomennd  46560  3f1oss1  47104  fafv2elrnb  47264  fmtnoinf  47550  nnsum4primeseven  47814  nnsum4primesevenALTV  47815  upgrimwlklem2  47911  upgrimwlklem3  47912  upgrimtrlslem2  47918  cycl3grtri  47959  domnmsuppn0  48344  scmsuppss  48346  fdivmpt  48520  fdivmptf  48521  refdivmptf  48522  fdivpm  48523  refdivpm  48524  elbigo2  48532  elbigolo1  48537