Theorem fndmd 6641

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

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

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 6540

This theorem is used by:  fdm  6716  f1dm  6781  f1odm  6825  f1o00  6857  fvelimad  6949  rescnvimafod  7070  f1eqcocnv  7306  ofrfvalg  7690  offval  7691  fndmexd  7905  dmmpoga  8076  fnwelem  8133  frrlem4  8292  frrlem8  8296  frrlem10  8298  fpr2  8307  fprresex  8313  wfr2  8330  tfrlem5  8372  ixpiunwdom  9566  frr2  9746  dfac12lem1  10150  ackbij2lem3  10246  itunisuc  10425  ttukeylem3  10517  prdsbas2  17560  prdsplusgval  17564  prdsmulrval  17566  prdsleval  17568  prdsvscaval  17570  imasleval  17633  ssclem  17914  isssc  17915  rescval2  17923  issubc2  17931  cofuval  17977  resfval2  17988  resf1st  17989  resf2nd  17990  prdsmgp  20290  lspextmo  21246  dsmmfi  21957  ofco2  22679  neiss2  23332  txdis1cn  23867  qtopcld  23945  qtoprest  23949  kqsat  23963  kqdisj  23964  isr0  23969  elfm3  24182  ovolunlem1  25731  ofpreima  33146  ofpreima2  33147  fnpreimac  33151  fsuppcurry1  33203  fsuppcurry2  33204  pfxf1  33396  cycpmfvlem  33560  cycpmfv1  33561  cycpmfv2  33562  cycpmfv3  33563  1arithidomlem2  33954  1arithidom  33955  esplyind  34093  ply1annidllem  34219  ofcfval  34616  probfinmeasb  34947  bnj564  35262  bnj1121  35502  bnj1442  35566  bnj1450  35567  bnj1501  35584  fnrelpredd  35604  onvfowev  35721  sdclem2  38500  prdstotbnd  38552  diadm  41916  dibdiadm  42036  dibdmN  42038  dicdmN  42065  dihdm  42150  aks4d1p1p5  42949  aks6d1c6lem2  43045  tfsconcat0b  44195  fnchoice  45871  wessf1ornlem  46025  limsupequzlem  46558  climrescn  46584  icccncfext  46723  stoweidlem35  46871  stoweidlem59  46895  smflimmpt  47646  smflimsuplem7  47662  iinfssclem1  49988  infsubc2d  49996  oppfvallem  50069  funcoppc3  50081  uptposlem  50131