Theorem fdm 6724

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

This proof depends on syntax axioms:   → wi 4   = wceq 1569  dom cdm 5651  ⟶wf 6539

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-fn 6546  df-f 6547

This theorem is used by:  fdmd  6725  fdmi  6726  fimacnv  6737  fssxp  6742  ffdm  6744  f00  6769  f0dom0  6771  f0rn0  6772  fimadmfo  6810  fimadmfoALT  6812  focofo  6814  feldmfvelcdm  7091  dff3  7105  ffvresb  7131  dmfex  7921  fiun  7959  soseq  8182  fsuppeq  8199  fsuppeqg  8200  issmo2  8364  smoiso  8377  mapprc  8858  elpm2r  8872  curf  8897  uncf  8898  map0b  8918  mapsnd  8921  brdomg  8992  pw2f1olem  9107  iunmapdisj  10109  fodomfi2  10146  infmap2  10302  coftr  10358  fin23lem40  10436  isf34lem7  10464  axdc3lem2  10536  axdc3lem4  10538  rpnnen1lem4  13115  rpnnen1lem5  13116  fseqsupcl  14127  fseqsupubi  14128  ello12  15692  lo1bdd  15696  elo12  15703  o1bdd  15707  lo1o1  15708  rlimclim  15722  ramval  17195  0ram2  17208  0ramcl  17210  intopsn  18841  mndpsuppss  18968  symgfixf1  19660  f1omvdconj  19669  pmtrdifellem1  19699  pmtrdifellem2  19700  gsumval3  20130  dprdss  20254  dmdprdsplitlem  20262  ablfaclem3  20312  evpmss  21901  pjdm2  22026  islindf2  22129  islindf4  22153  matunitlindflem2  23004  decpmatval  23092  pmatcollpw3lem  23110  iscnp3  23571  cnpnei  23591  cncls2  23600  cncls  23601  cnntr  23602  cncnp  23607  cndis  23618  paste  23621  cncmp  23719  imacmp  23724  hauscmplem  23733  cnconn  23749  kgencn  23884  xkopt  23983  xkococnlem  23987  fbasrn  24212  fmval  24271  fmf  24273  rnelfmlem  24280  rnelfm  24281  cnflf2  24331  psmetdmdm  24633  xmetres  24692  metres  24693  metcnp  24869  metustsym  24883  cfilucfil  24887  metuel2  24893  iscauf  25610  equivcau  25630  lmclimf  25634  ismbf  25958  ismbfcn  25959  mbfimaicc  25961  mbfimaopn2  25987  ibl0  26116  cniccibl  26170  cnicciblnc  26172  dvnfre  26281  c1liplem1  26325  c1lip2  26327  dvcnvrelem2  26347  plyco0  26519  plyeq0  26539  vieta1lem2  26643  ulm2  26721  ulmss  26733  ulmdvlem2  26737  ulmdvlem3  26738  itgulm  26744  basellem5  27421  nodmon  28016  newbdayim  28298  eedimeq  29485  axcontlem10  29560  wlkn0  30210  wlkres  30258  wlkp1lem1  30261  pthdivtx  30321  cyclnumvtx  30397  dmadjrnb  32517  elnlfn  32539  xppreima  33290  indpreima  33482  symgcom2  33695  tocyc01  33729  tocyccntz  33755  elrspunidl  34028  smatrcl  34478  mdetpmtr1  34505  locfinreflem  34522  hauseqcn  34580  rge0scvg  34631  isrnmeas  34883  omsfval  34976  omscl  34977  omsf  34978  eulerpartlemv  35046  eulerpartlemd  35048  eulerpartlemb  35050  eulerpartlemr  35056  eulerpartlemgvv  35058  eulerpartlemgs2  35062  eulerpartlemn  35063  rpsqrtcn  35272  cvmlift2lem9  36166  cvmlift3lem7  36180  mrsubfval  36363  ivthALT  37219  unccur  38635  ptrecube  38647  heicant  38682  mbfresfi  38693  itg2addnclem  38698  itg2addnclem2  38699  ftc1anclem1  38720  indexdom  38777  sdclem2  38785  cnres2  38806  sstotbnd2  38817  bnd2lem  38834  ismgmOLD  38893  ismndo2  38917  exidreslem  38920  rngosn3  38967  rngodm1dm2  38975  rhmqusspan  43344  coeq0i  43873  pw2f1ocnv  44153  cnioobibld  44325  dfno2  44538  fresin2  46295  evthiccabs  46616  dvsubcncf  47042  dvmulcncf  47043  dvdivcncf  47045  cnbdibl  47080  fourierdlem48  47272  fourierdlem49  47273  fourierdlem58  47282  fourierdlem59  47283  fourierdlem71  47295  fourierdlem73  47297  fourierdlem74  47298  fourierdlem75  47299  fourierdlem76  47300  fourierdlem80  47304  fourierdlem81  47305  fourierdlem89  47313  fourierdlem91  47315  fourierdlem92  47316  fourierdlem93  47317  fourierdlem94  47318  fourierdlem111  47335  fourierdlem112  47336  fourierdlem113  47337  fouriercn  47350  sge0val  47484  fge0iccico  47488  isomennd  47649  tannpoly  48048  3f1oss1  48253  fafv2elrnb  48413  fmtnoinf  48729  nnsum4primeseven  49006  nnsum4primesevenALTV  49007  upgrimwlklem2  49104  upgrimwlklem3  49105  upgrimtrlslem2  49111  cycl3grtri  49153  domnmsuppn0  49589  scmsuppss  49591  fdivmpt  49760  fdivmptf  49761  refdivmptf  49762  fdivpm  49763  refdivpm  49764  elbigo2  49772  elbigolo1  49777  xpco2  50076