Theorem fndmd 6630

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

Syntax hints:   → wi 4   = wceq 1563  dom cdm 5652   Fn wfn 6520

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 401  df-fn 6528

This theorem is referenced by:  fdm  6705  f1dm  6770  f1odm  6814  f1o00  6846  fvelimad  6938  rescnvimafod  7058  f1eqcocnv  7289  ofrfvalg  7672  offval  7673  fndmexd  7889  dmmpoga  8058  fnwelem  8115  frrlem4  8274  frrlem8  8278  frrlem10  8280  fpr2  8289  fprresex  8295  wfr2  8312  tfrlem5  8354  ixpiunwdom  9540  frr2  9720  dfac12lem1  10115  ackbij2lem3  10211  itunisuc  10391  ttukeylem3  10483  prdsbas2  17512  prdsplusgval  17516  prdsmulrval  17518  prdsleval  17520  prdsvscaval  17522  imasleval  17585  ssclem  17866  isssc  17867  rescval2  17875  issubc2  17883  cofuval  17929  resfval2  17940  resf1st  17941  resf2nd  17942  prdsmgp  20218  lspextmo  21146  dsmmfi  21848  ofco2  22569  neiss2  23219  txdis1cn  23753  qtopcld  23831  qtoprest  23835  kqsat  23849  kqdisj  23850  isr0  23855  elfm3  24068  ovolunlem1  25617  ofpreima  32922  ofpreima2  32923  fnpreimac  32927  fsuppcurry1  32981  fsuppcurry2  32982  pfxf1  33175  s2rnOLD  33177  s3rnOLD  33179  cycpmfvlem  33345  cycpmfv1  33346  cycpmfv2  33347  cycpmfv3  33348  1arithidomlem2  33743  1arithidom  33744  esplyind  33882  ply1annidllem  34008  ofcfval  34405  probfinmeasb  34735  bnj564  35050  bnj1121  35290  bnj1442  35354  bnj1450  35355  bnj1501  35372  fnrelpredd  35397  onvfowev  35471  sdclem2  38253  prdstotbnd  38305  diadm  41671  dibdiadm  41791  dibdmN  41793  dicdmN  41820  dihdm  41905  aks4d1p1p5  42704  aks6d1c6lem2  42800  tfsconcat0b  43935  fnchoice  45607  wessf1ornlem  45761  limsupequzlem  46294  climrescn  46320  icccncfext  46459  stoweidlem35  46607  stoweidlem59  46631  smflimmpt  47382  smflimsuplem7  47398  iinfssclem1  49683  infsubc2d  49691  oppfvallem  49764  funcoppc3  49776  uptposlem  49826