Theorem fdm 6495

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

Syntax hints:   → wi 4   = wceq 1538  dom cdm 5519  ⟶wf 6320

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 210  df-an 400  df-fn 6327  df-f 6328

This theorem is referenced by:  fdmd  6497  fdmi  6498  fssxp  6508  ffdm  6510  f00  6535  f0dom0  6537  f0rn0  6538  fimadmfo  6574  fimadmfoALT  6576  foco  6577  fimacnv  6816  dff3  6843  ffvresb  6865  dmfex  7623  fiun  7626  frnsuppeq  7825  suppss  7843  issmo2  7969  smoiso  7982  mapprc  8393  elpm2r  8407  map0b  8430  mapsnd  8433  brdomg  8502  pw2f1olem  8604  iunmapdisj  9434  fodomfi2  9471  infmap2  9629  coftr  9684  fin23lem40  9762  isf34lem7  9790  axdc3lem2  9862  axdc3lem4  9864  rpnnen1lem4  12367  rpnnen1lem5  12368  fseqsupcl  13340  fseqsupubi  13341  ello12  14865  lo1bdd  14869  elo12  14876  o1bdd  14880  lo1o1  14881  rlimclim  14895  ramval  16334  0ram2  16347  0ramcl  16349  intopsn  17856  symgfixf1  18557  f1omvdconj  18566  pmtrdifellem1  18596  pmtrdifellem2  18597  gsumval3  19020  dprdss  19144  dmdprdsplitlem  19152  ablfaclem3  19202  evpmss  20275  pjdm2  20400  islindf2  20503  islindf4  20527  decpmatval  21370  pmatcollpw3lem  21388  iscnp3  21849  cnpnei  21869  cncls2  21878  cncls  21879  cnntr  21880  cncnp  21885  cndis  21896  paste  21899  cncmp  21997  imacmp  22002  hauscmplem  22011  cnconn  22027  kgencn  22161  xkopt  22260  xkococnlem  22264  fbasrn  22489  fmval  22548  fmf  22550  rnelfmlem  22557  rnelfm  22558  cnflf2  22608  psmetdmdm  22912  xmetres  22971  metres  22972  metcnp  23148  metustsym  23162  cfilucfil  23166  metuel2  23172  iscauf  23884  equivcau  23904  lmclimf  23908  ismbf  24232  ismbfcn  24233  mbfimaicc  24235  mbfimaopn2  24261  ibl0  24390  cniccibl  24444  cnicciblnc  24446  dvnfre  24555  c1liplem1  24599  c1lip2  24601  dvcnvrelem2  24621  plyco0  24789  plyeq0  24808  vieta1lem2  24907  ulm2  24980  ulmss  24992  ulmdvlem2  24996  ulmdvlem3  24997  itgulm  25003  basellem5  25670  eedimeq  26692  axcontlem10  26767  wlkn0  27410  wlkres  27460  wlkp1lem1  27463  pthdivtx  27518  dmadjrnb  29689  elnlfn  29711  xppreima  30408  symgcom2  30778  tocyc01  30810  tocyccntz  30836  elrspunidl  31014  smatrcl  31149  mdetpmtr1  31176  locfinreflem  31193  hauseqcn  31251  rge0scvg  31302  indpreima  31394  isrnmeas  31569  omsfval  31662  omscl  31663  omsf  31664  eulerpartlemv  31732  eulerpartlemd  31734  eulerpartlemb  31736  eulerpartlemr  31742  eulerpartlemgvv  31744  eulerpartlemgs2  31748  eulerpartlemn  31749  rpsqrtcn  31974  cvmlift2lem9  32671  cvmlift3lem7  32685  mrsubfval  32868  soseq  33209  nodmon  33270  ivthALT  33796  curf  35035  uncf  35036  unccur  35040  matunitlindflem2  35054  ptrecube  35057  heicant  35092  mbfresfi  35103  itg2addnclem  35108  itg2addnclem2  35109  ftc1anclem1  35130  indexdom  35172  sdclem2  35180  cnres2  35201  sstotbnd2  35212  bnd2lem  35229  ismgmOLD  35288  ismndo2  35312  exidreslem  35315  rngosn3  35362  rngodm1dm2  35370  coeq0i  39694  pw2f1ocnv  39978  cnioobibld  40164  fresin2  41796  evthiccabs  42133  dvsubcncf  42566  dvmulcncf  42567  dvdivcncf  42569  cnbdibl  42604  fourierdlem48  42796  fourierdlem49  42797  fourierdlem58  42806  fourierdlem59  42807  fourierdlem71  42819  fourierdlem73  42821  fourierdlem74  42822  fourierdlem75  42823  fourierdlem76  42824  fourierdlem80  42828  fourierdlem81  42829  fourierdlem89  42837  fourierdlem91  42839  fourierdlem92  42840  fourierdlem93  42841  fourierdlem94  42842  fourierdlem111  42859  fourierdlem112  42860  fourierdlem113  42861  fouriercn  42874  sge0val  43005  fge0iccico  43009  isomennd  43170  fafv2elrnb  43791  fmtnoinf  44053  nnsum4primeseven  44318  nnsum4primesevenALTV  44319  domnmsuppn0  44771  mndpsuppss  44773  scmsuppss  44774  fdivmpt  44954  fdivmptf  44955  refdivmptf  44956  fdivpm  44957  refdivpm  44958  elbigo2  44966  elbigolo1  44971