Theorem fndmd 6655

Description: The domain of a function. (Contributed by Glauco Siliprandi, 23-Oct-2021.)

Hypothesis

Ref	Expression
fndmd.1	⊢ (𝜑 → 𝐹 Fn 𝐴)

Assertion

Ref	Expression
fndmd	⊢ (𝜑 → dom 𝐹 = 𝐴)

Proof of Theorem fndmd

Step	Hyp	Ref	Expression
1		fndmd.1	. 2 ⊢ (𝜑 → 𝐹 Fn 𝐴)
2		fndm 6653	. 2 ⊢ (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴)
3	1, 2	syl 17	1 ⊢ (𝜑 → dom 𝐹 = 𝐴)

Syntax hints:   → wi 4   = wceq 1542  dom cdm 5677   Fn wfn 6539

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

This theorem is referenced by:  fdm  6727  f1dm  6792  f1o00  6869  fvelimad  6960  rescnvimafod  7076  f1eqcocnv  7299  ofrfvalg  7678  offval  7679  fndmexd  7897  dmmpoga  8059  fnwelem  8117  frrlem4  8274  frrlem8  8278  frrlem10  8280  fpr2  8289  fprresex  8295  wfrlem17OLD  8325  wfr2  8336  tfrlem5  8380  ixpiunwdom  9585  frr2  9755  dfac12lem1  10138  ackbij2lem3  10236  itunisuc  10414  ttukeylem3  10506  prdsbas2  17415  prdsplusgval  17419  prdsmulrval  17421  prdsleval  17423  prdsvscaval  17425  imasleval  17487  ssclem  17766  isssc  17767  rescval2  17775  issubc2  17786  cofuval  17832  resfval2  17843  resf1st  17844  resf2nd  17845  prdsmgp  20132  lspextmo  20667  dsmmfi  21293  ofco2  21953  neiss2  22605  txdis1cn  23139  qtopcld  23217  qtoprest  23221  kqsat  23235  kqdisj  23236  isr0  23241  elfm3  23454  ovolunlem1  25014  ofpreima  31890  ofpreima2  31891  fnpreimac  31896  fsuppcurry1  31950  fsuppcurry2  31951  pfxf1  32108  s2rn  32110  s3rn  32112  cycpmfvlem  32271  cycpmfv1  32272  cycpmfv2  32273  cycpmfv3  32274  ply1annidllem  32762  ofcfval  33096  probfinmeasb  33427  bnj564  33755  bnj1121  33996  bnj1442  34060  bnj1450  34061  bnj1501  34078  fnrelpredd  34092  sdclem2  36610  prdstotbnd  36662  diadm  39906  dibdiadm  40026  dibdmN  40028  dicdmN  40055  dihdm  40140  aks4d1p1p5  40940  tfsconcat0b  42096  fnchoice  43713  wessf1ornlem  43882  limsupequzlem  44438  climrescn  44464  icccncfext  44603  stoweidlem35  44751  stoweidlem59  44775  smflimmpt  45526  smflimsuplem7  45542