Theorem fndmd 6427

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

Syntax hints:   → wi 4   = wceq 1538  dom cdm 5519   Fn wfn 6319

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 210  df-an 400  df-fn 6327

This theorem is referenced by:  fdm  6495  f1dm  6553  f1o00  6624  fvelimad  6707  f1eqcocnv  7035  offval  7396  ofrfval  7397  fndmexd  7597  dmmpoga  7753  fnwelem  7808  wfrlem17  7954  tfrlem5  7999  ixpiunwdom  9038  dfac12lem1  9554  ackbij2lem3  9652  itunisuc  9830  ttukeylem3  9922  prdsbas2  16734  prdsplusgval  16738  prdsmulrval  16740  prdsleval  16742  prdsvscaval  16744  imasleval  16806  ssclem  17081  isssc  17082  rescval2  17090  issubc2  17098  cofuval  17144  resfval2  17155  resf1st  17156  resf2nd  17157  prdsmgp  19356  lspextmo  19821  dsmmfi  20427  ofco2  21056  neiss2  21706  txdis1cn  22240  qtopcld  22318  qtoprest  22322  kqsat  22336  kqdisj  22337  isr0  22342  elfm3  22555  ovolunlem1  24101  ofpreima  30428  ofpreima2  30429  fnpreimac  30434  fsuppcurry1  30487  fsuppcurry2  30488  pfxf1  30644  s2rn  30646  s3rn  30648  cycpmfvlem  30804  cycpmfv1  30805  cycpmfv2  30806  cycpmfv3  30807  ofcfval  31467  probfinmeasb  31796  bnj564  32125  bnj1121  32367  bnj1442  32431  bnj1450  32432  bnj1501  32449  fnrelpredd  32472  frrlem4  33239  frrlem8  33243  frrlem10  33245  fpr2  33253  frr2  33258  sdclem2  35180  prdstotbnd  35232  diadm  38331  dibdiadm  38451  dibdmN  38453  dicdmN  38480  dihdm  38565  fnchoice  41658  wessf1ornlem  41811  limsupequzlem  42364  climrescn  42390  icccncfext  42529  stoweidlem35  42677  stoweidlem59  42701  smflimmpt  43441  smflimsuplem7  43457