Theorem fndmd 6586

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 6584	. 2 ⊢ (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴)
3	1, 2	syl 17	1 ⊢ (𝜑 → dom 𝐹 = 𝐴)

Syntax hints:   → wi 4   = wceq 1541  dom cdm 5616   Fn wfn 6476

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 6484

This theorem is referenced by:  fdm  6660  f1dm  6723  f1o00  6798  fvelimad  6889  rescnvimafod  7006  f1eqcocnv  7235  ofrfvalg  7618  offval  7619  fndmexd  7834  dmmpoga  8005  fnwelem  8061  frrlem4  8219  frrlem8  8223  frrlem10  8225  fpr2  8234  fprresex  8240  wfr2  8257  tfrlem5  8299  ixpiunwdom  9476  frr2  9650  dfac12lem1  10032  ackbij2lem3  10128  itunisuc  10307  ttukeylem3  10399  prdsbas2  17370  prdsplusgval  17374  prdsmulrval  17376  prdsleval  17378  prdsvscaval  17380  imasleval  17442  ssclem  17723  isssc  17724  rescval2  17732  issubc2  17740  cofuval  17786  resfval2  17797  resf1st  17798  resf2nd  17799  prdsmgp  20067  lspextmo  20988  dsmmfi  21673  ofco2  22364  neiss2  23014  txdis1cn  23548  qtopcld  23626  qtoprest  23630  kqsat  23644  kqdisj  23645  isr0  23650  elfm3  23863  ovolunlem1  25423  ofpreima  32642  ofpreima2  32643  fnpreimac  32648  fsuppcurry1  32702  fsuppcurry2  32703  pfxf1  32918  s2rnOLD  32920  s3rnOLD  32922  cycpmfvlem  33076  cycpmfv1  33077  cycpmfv2  33078  cycpmfv3  33079  1arithidomlem2  33496  1arithidom  33497  ply1annidllem  33709  ofcfval  34106  probfinmeasb  34436  bnj564  34751  bnj1121  34992  bnj1442  35056  bnj1450  35057  bnj1501  35074  fnrelpredd  35097  sdclem2  37781  prdstotbnd  37833  diadm  41073  dibdiadm  41193  dibdmN  41195  dicdmN  41222  dihdm  41307  aks4d1p1p5  42107  aks6d1c6lem2  42203  tfsconcat0b  43378  fnchoice  45065  wessf1ornlem  45221  limsupequzlem  45759  climrescn  45785  icccncfext  45924  stoweidlem35  46072  stoweidlem59  46096  smflimmpt  46847  smflimsuplem7  46863  iinfssclem1  49085  infsubc2d  49093  oppfvallem  49166  funcoppc3  49178  uptposlem  49228