Theorem fndmd 6684

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

Syntax hints:   → wi 4   = wceq 1537  dom cdm 5700   Fn wfn 6568

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 6576

This theorem is referenced by:  fdm  6756  f1dm  6821  f1o00  6897  fvelimad  6989  rescnvimafod  7107  f1eqcocnv  7337  ofrfvalg  7722  offval  7723  fndmexd  7944  dmmpoga  8114  fnwelem  8172  frrlem4  8330  frrlem8  8334  frrlem10  8336  fpr2  8345  fprresex  8351  wfrlem17OLD  8381  wfr2  8392  tfrlem5  8436  ixpiunwdom  9659  frr2  9829  dfac12lem1  10213  ackbij2lem3  10309  itunisuc  10488  ttukeylem3  10580  prdsbas2  17529  prdsplusgval  17533  prdsmulrval  17535  prdsleval  17537  prdsvscaval  17539  imasleval  17601  ssclem  17880  isssc  17881  rescval2  17889  issubc2  17900  cofuval  17946  resfval2  17957  resf1st  17958  resf2nd  17959  prdsmgp  20178  lspextmo  21078  dsmmfi  21781  ofco2  22478  neiss2  23130  txdis1cn  23664  qtopcld  23742  qtoprest  23746  kqsat  23760  kqdisj  23761  isr0  23766  elfm3  23979  ovolunlem1  25551  ofpreima  32683  ofpreima2  32684  fnpreimac  32689  fsuppcurry1  32739  fsuppcurry2  32740  pfxf1  32908  s2rnOLD  32910  s3rnOLD  32912  cycpmfvlem  33105  cycpmfv1  33106  cycpmfv2  33107  cycpmfv3  33108  1arithidomlem2  33529  1arithidom  33530  ply1annidllem  33694  ofcfval  34062  probfinmeasb  34393  bnj564  34720  bnj1121  34961  bnj1442  35025  bnj1450  35026  bnj1501  35043  fnrelpredd  35065  sdclem2  37702  prdstotbnd  37754  diadm  40992  dibdiadm  41112  dibdmN  41114  dicdmN  41141  dihdm  41226  aks4d1p1p5  42032  aks6d1c6lem2  42128  tfsconcat0b  43308  fnchoice  44929  wessf1ornlem  45092  limsupequzlem  45643  climrescn  45669  icccncfext  45808  stoweidlem35  45956  stoweidlem59  45980  smflimmpt  46731  smflimsuplem7  46747