Theorem fndmd 6673

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

Syntax hints:   → wi 4   = wceq 1540  dom cdm 5685   Fn wfn 6556

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 207  df-an 396  df-fn 6564

This theorem is referenced by:  fdm  6745  f1dm  6808  f1o00  6883  fvelimad  6976  rescnvimafod  7093  f1eqcocnv  7321  ofrfvalg  7705  offval  7706  fndmexd  7926  dmmpoga  8098  fnwelem  8156  frrlem4  8314  frrlem8  8318  frrlem10  8320  fpr2  8329  fprresex  8335  wfrlem17OLD  8365  wfr2  8376  tfrlem5  8420  ixpiunwdom  9630  frr2  9800  dfac12lem1  10184  ackbij2lem3  10280  itunisuc  10459  ttukeylem3  10551  prdsbas2  17514  prdsplusgval  17518  prdsmulrval  17520  prdsleval  17522  prdsvscaval  17524  imasleval  17586  ssclem  17863  isssc  17864  rescval2  17872  issubc2  17881  cofuval  17927  resfval2  17938  resf1st  17939  resf2nd  17940  prdsmgp  20148  lspextmo  21055  dsmmfi  21758  ofco2  22457  neiss2  23109  txdis1cn  23643  qtopcld  23721  qtoprest  23725  kqsat  23739  kqdisj  23740  isr0  23745  elfm3  23958  ovolunlem1  25532  ofpreima  32675  ofpreima2  32676  fnpreimac  32681  fsuppcurry1  32736  fsuppcurry2  32737  pfxf1  32926  s2rnOLD  32928  s3rnOLD  32930  cycpmfvlem  33132  cycpmfv1  33133  cycpmfv2  33134  cycpmfv3  33135  1arithidomlem2  33564  1arithidom  33565  ply1annidllem  33744  ofcfval  34099  probfinmeasb  34430  bnj564  34758  bnj1121  34999  bnj1442  35063  bnj1450  35064  bnj1501  35081  fnrelpredd  35103  sdclem2  37749  prdstotbnd  37801  diadm  41037  dibdiadm  41157  dibdmN  41159  dicdmN  41186  dihdm  41271  aks4d1p1p5  42076  aks6d1c6lem2  42172  tfsconcat0b  43359  fnchoice  45034  wessf1ornlem  45190  limsupequzlem  45737  climrescn  45763  icccncfext  45902  stoweidlem35  46050  stoweidlem59  46074  smflimmpt  46825  smflimsuplem7  46841