Theorem fndmd 6669

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570  dom cdm 5656   Fn wfn 6556

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-fn 6564

This theorem is used by:  fdm  6744  f1dm  6809  f1odm  6853  f1o00  6886  fvelimad  6978  rescnvimafod  7100  f1eqcocnv  7335  ofrfvalg  7728  offval  7729  fndmexd  7943  dmmpoga  8114  fnwelem  8173  frrlem4  8338  frrlem8  8342  frrlem10  8344  fpr2  8353  fprresex  8359  wfr2  8376  tfrlem5  8418  ixpiunwdom  9614  frr2  9794  dfac12lem1  10252  ackbij2lem3  10348  itunisuc  10527  ttukeylem3  10619  prdsbas2  17672  prdsplusgval  17676  prdsmulrval  17678  prdsleval  17680  prdsvscaval  17682  imasleval  17745  ssclem  18026  isssc  18027  rescval2  18035  issubc2  18043  cofuval  18089  resfval2  18100  resf1st  18101  resf2nd  18102  prdsmgp  20404  lspextmo  21364  dsmmfi  22077  ofco2  22799  neiss2  23452  txdis1cn  23987  qtopcld  24065  qtoprest  24069  kqsat  24083  kqdisj  24084  isr0  24089  elfm3  24302  ovolunlem1  25851  ofpreima  33334  ofpreima2  33335  fnpreimac  33339  fsuppcurry1  33389  fsuppcurry2  33390  pfxf1  33582  cycpmfvlem  33749  cycpmfv1  33750  cycpmfv2  33751  cycpmfv3  33752  1arithidomlem2  34152  1arithidom  34153  esplyind  34290  ply1annidllem  34416  ofcfval  34813  probfinmeasb  35143  bnj564  35458  bnj1121  35698  bnj1442  35762  bnj1450  35763  bnj1501  35780  fnrelpredd  35817  onvfowev  36063  sdclem2  38879  prdstotbnd  38931  diadm  42295  dibdiadm  42415  dibdmN  42417  dicdmN  42444  dihdm  42529  aks4d1p1p5  43328  aks6d1c6lem2  43424  tfsconcat0b  44551  fnchoice  46262  wessf1ornlem  46415  limsupequzlem  46947  climrescn  46973  icccncfext  47112  stoweidlem35  47260  stoweidlem59  47284  smflimmpt  48035  smflimsuplem7  48051  iinfssclem1  50383  infsubc2d  50391  oppfvallem  50466  funcoppc3  50478  uptposlem  50528