Theorem fndmd 6597

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

Syntax hints:   → wi 4   = wceq 1547  dom cdm 5625   Fn wfn 6487

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 208  df-an 397  df-fn 6495

This theorem is referenced by:  fdm  6671  f1dm  6734  f1o00  6809  fvelimad  6901  rescnvimafod  7021  f1eqcocnv  7252  ofrfvalg  7635  offval  7636  fndmexd  7851  dmmpoga  8022  fnwelem  8078  frrlem4  8236  frrlem8  8240  frrlem10  8242  fpr2  8251  fprresex  8257  wfr2  8274  tfrlem5  8316  ixpiunwdom  9502  frr2  9682  dfac12lem1  10064  ackbij2lem3  10160  itunisuc  10339  ttukeylem3  10431  prdsbas2  17430  prdsplusgval  17434  prdsmulrval  17436  prdsleval  17438  prdsvscaval  17440  imasleval  17503  ssclem  17784  isssc  17785  rescval2  17793  issubc2  17801  cofuval  17847  resfval2  17858  resf1st  17859  resf2nd  17860  prdsmgp  20130  lspextmo  21053  dsmmfi  21720  ofco2  22441  neiss2  23091  txdis1cn  23625  qtopcld  23703  qtoprest  23707  kqsat  23721  kqdisj  23722  isr0  23727  elfm3  23940  ovolunlem1  25489  ofpreima  32764  ofpreima2  32765  fnpreimac  32769  fsuppcurry1  32823  fsuppcurry2  32824  pfxf1  33028  s2rnOLD  33030  s3rnOLD  33032  cycpmfvlem  33200  cycpmfv1  33201  cycpmfv2  33202  cycpmfv3  33203  1arithidomlem2  33626  1arithidom  33627  esplyind  33766  ply1annidllem  33892  ofcfval  34289  probfinmeasb  34619  bnj564  34934  bnj1121  35174  bnj1442  35238  bnj1450  35239  bnj1501  35256  fnrelpredd  35279  sdclem2  38116  prdstotbnd  38168  diadm  41534  dibdiadm  41654  dibdmN  41656  dicdmN  41683  dihdm  41768  aks4d1p1p5  42567  aks6d1c6lem2  42663  tfsconcat0b  43798  fnchoice  45484  wessf1ornlem  45639  limsupequzlem  46172  climrescn  46198  icccncfext  46337  stoweidlem35  46485  stoweidlem59  46509  smflimmpt  47260  smflimsuplem7  47276  iinfssclem1  49551  infsubc2d  49559  oppfvallem  49632  funcoppc3  49644  uptposlem  49694