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  31921  ofpreima2  31922  fnpreimac  31927  fsuppcurry1  31981  fsuppcurry2  31982  pfxf1  32139  s2rn  32141  s3rn  32143  cycpmfvlem  32302  cycpmfv1  32303  cycpmfv2  32304  cycpmfv3  32305  ply1annidllem  32793  ofcfval  33127  probfinmeasb  33458  bnj564  33786  bnj1121  34027  bnj1442  34091  bnj1450  34092  bnj1501  34109  fnrelpredd  34123  sdclem2  36658  prdstotbnd  36710  diadm  39954  dibdiadm  40074  dibdmN  40076  dicdmN  40103  dihdm  40188  aks4d1p1p5  40988  tfsconcat0b  42144  fnchoice  43761  wessf1ornlem  43930  limsupequzlem  44486  climrescn  44512  icccncfext  44651  stoweidlem35  44799  stoweidlem59  44823  smflimmpt  45574  smflimsuplem7  45590