Theorem fdm 6671

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

Syntax hints:   → wi 4   = wceq 1542  dom cdm 5624  ⟶wf 6488

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 6495  df-f 6496

This theorem is referenced by:  fdmd  6672  fdmi  6673  fimacnv  6684  fssxp  6689  ffdm  6691  f00  6716  f0dom0  6718  f0rn0  6719  fimadmfo  6755  fimadmfoALT  6757  focofo  6759  feldmfvelcdm  7032  dff3  7046  ffvresb  7072  dmfex  7849  fiun  7889  soseq  8102  fsuppeq  8118  fsuppeqg  8119  issmo2  8282  smoiso  8295  mapprc  8770  elpm2r  8785  map0b  8824  mapsnd  8827  brdomg  8898  pw2f1olem  9012  iunmapdisj  9936  fodomfi2  9973  infmap2  10130  coftr  10186  fin23lem40  10264  isf34lem7  10292  axdc3lem2  10364  axdc3lem4  10366  rpnnen1lem4  12921  rpnnen1lem5  12922  fseqsupcl  13930  fseqsupubi  13931  ello12  15469  lo1bdd  15473  elo12  15480  o1bdd  15484  lo1o1  15485  rlimclim  15499  ramval  16970  0ram2  16983  0ramcl  16985  intopsn  18613  mndpsuppss  18724  symgfixf1  19403  f1omvdconj  19412  pmtrdifellem1  19442  pmtrdifellem2  19443  gsumval3  19873  dprdss  19997  dmdprdsplitlem  20005  ablfaclem3  20055  evpmss  21576  pjdm2  21701  islindf2  21804  islindf4  21828  decpmatval  22740  pmatcollpw3lem  22758  iscnp3  23219  cnpnei  23239  cncls2  23248  cncls  23249  cnntr  23250  cncnp  23255  cndis  23266  paste  23269  cncmp  23367  imacmp  23372  hauscmplem  23381  cnconn  23397  kgencn  23531  xkopt  23630  xkococnlem  23634  fbasrn  23859  fmval  23918  fmf  23920  rnelfmlem  23927  rnelfm  23928  cnflf2  23978  psmetdmdm  24280  xmetres  24339  metres  24340  metcnp  24516  metustsym  24530  cfilucfil  24534  metuel2  24540  iscauf  25257  equivcau  25277  lmclimf  25281  ismbf  25605  ismbfcn  25606  mbfimaicc  25608  mbfimaopn2  25634  ibl0  25764  cniccibl  25818  cnicciblnc  25820  dvnfre  25929  c1liplem1  25973  c1lip2  25975  dvcnvrelem2  25995  plyco0  26167  plyeq0  26186  vieta1lem2  26288  ulm2  26363  ulmss  26375  ulmdvlem2  26379  ulmdvlem3  26380  itgulm  26386  basellem5  27062  nodmon  27628  newbdayim  27909  eedimeq  28981  axcontlem10  29056  wlkn0  29704  wlkres  29752  wlkp1lem1  29755  pthdivtx  29810  cyclnumvtx  29883  dmadjrnb  31992  elnlfn  32014  xppreima  32733  indpreima  32940  symgcom2  33160  tocyc01  33194  tocyccntz  33220  elrspunidl  33503  smatrcl  33956  mdetpmtr1  33983  locfinreflem  34000  hauseqcn  34058  rge0scvg  34109  isrnmeas  34360  omsfval  34454  omscl  34455  omsf  34456  eulerpartlemv  34524  eulerpartlemd  34526  eulerpartlemb  34528  eulerpartlemr  34534  eulerpartlemgvv  34536  eulerpartlemgs2  34540  eulerpartlemn  34541  rpsqrtcn  34753  cvmlift2lem9  35509  cvmlift3lem7  35523  mrsubfval  35706  ivthALT  36533  curf  37933  uncf  37934  unccur  37938  matunitlindflem2  37952  ptrecube  37955  heicant  37990  mbfresfi  38001  itg2addnclem  38006  itg2addnclem2  38007  ftc1anclem1  38028  indexdom  38069  sdclem2  38077  cnres2  38098  sstotbnd2  38109  bnd2lem  38126  ismgmOLD  38185  ismndo2  38209  exidreslem  38212  rngosn3  38259  rngodm1dm2  38267  rhmqusspan  42638  coeq0i  43199  pw2f1ocnv  43483  cnioobibld  43660  dfno2  43873  fresin2  45620  evthiccabs  45944  dvsubcncf  46370  dvmulcncf  46371  dvdivcncf  46373  cnbdibl  46408  fourierdlem48  46600  fourierdlem49  46601  fourierdlem58  46610  fourierdlem59  46611  fourierdlem71  46623  fourierdlem73  46625  fourierdlem74  46626  fourierdlem75  46627  fourierdlem76  46628  fourierdlem80  46632  fourierdlem81  46633  fourierdlem89  46641  fourierdlem91  46643  fourierdlem92  46644  fourierdlem93  46645  fourierdlem94  46646  fourierdlem111  46663  fourierdlem112  46664  fourierdlem113  46665  fouriercn  46678  sge0val  46812  fge0iccico  46816  isomennd  46977  tannpoly  47350  3f1oss1  47535  fafv2elrnb  47695  fmtnoinf  48011  nnsum4primeseven  48288  nnsum4primesevenALTV  48289  upgrimwlklem2  48386  upgrimwlklem3  48387  upgrimtrlslem2  48393  cycl3grtri  48435  domnmsuppn0  48857  scmsuppss  48859  fdivmpt  49028  fdivmptf  49029  refdivmptf  49030  fdivpm  49031  refdivpm  49032  elbigo2  49040  elbigolo1  49045  xpco2  49344