Theorem fndmd 6673

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

Syntax hints:   → wi 4   = wceq 1536  dom cdm 5688   Fn wfn 6557

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 6565

This theorem is referenced by:  fdm  6745  f1dm  6808  f1o00  6883  fvelimad  6975  rescnvimafod  7092  f1eqcocnv  7320  ofrfvalg  7704  offval  7705  fndmexd  7926  dmmpoga  8096  fnwelem  8154  frrlem4  8312  frrlem8  8316  frrlem10  8318  fpr2  8327  fprresex  8333  wfrlem17OLD  8363  wfr2  8374  tfrlem5  8418  ixpiunwdom  9627  frr2  9797  dfac12lem1  10181  ackbij2lem3  10277  itunisuc  10456  ttukeylem3  10548  prdsbas2  17515  prdsplusgval  17519  prdsmulrval  17521  prdsleval  17523  prdsvscaval  17525  imasleval  17587  ssclem  17866  isssc  17867  rescval2  17875  issubc2  17886  cofuval  17932  resfval2  17943  resf1st  17944  resf2nd  17945  prdsmgp  20168  lspextmo  21072  dsmmfi  21775  ofco2  22472  neiss2  23124  txdis1cn  23658  qtopcld  23736  qtoprest  23740  kqsat  23754  kqdisj  23755  isr0  23760  elfm3  23973  ovolunlem1  25545  ofpreima  32681  ofpreima2  32682  fnpreimac  32687  fsuppcurry1  32742  fsuppcurry2  32743  pfxf1  32910  s2rnOLD  32912  s3rnOLD  32914  cycpmfvlem  33114  cycpmfv1  33115  cycpmfv2  33116  cycpmfv3  33117  1arithidomlem2  33543  1arithidom  33544  ply1annidllem  33708  ofcfval  34078  probfinmeasb  34409  bnj564  34736  bnj1121  34977  bnj1442  35041  bnj1450  35042  bnj1501  35059  fnrelpredd  35081  sdclem2  37728  prdstotbnd  37780  diadm  41017  dibdiadm  41137  dibdmN  41139  dicdmN  41166  dihdm  41251  aks4d1p1p5  42056  aks6d1c6lem2  42152  tfsconcat0b  43335  fnchoice  44966  wessf1ornlem  45127  limsupequzlem  45677  climrescn  45703  icccncfext  45842  stoweidlem35  45990  stoweidlem59  46014  smflimmpt  46765  smflimsuplem7  46781