Theorem fndmd 6597

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

Syntax hints:   → wi 4   = wceq 1541  dom cdm 5624   Fn wfn 6487

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 6495

This theorem is referenced by:  fdm  6671  f1dm  6734  f1o00  6809  fvelimad  6901  rescnvimafod  7018  f1eqcocnv  7247  ofrfvalg  7630  offval  7631  fndmexd  7846  dmmpoga  8017  fnwelem  8073  frrlem4  8231  frrlem8  8235  frrlem10  8237  fpr2  8246  fprresex  8252  wfr2  8269  tfrlem5  8311  ixpiunwdom  9495  frr2  9672  dfac12lem1  10054  ackbij2lem3  10150  itunisuc  10329  ttukeylem3  10421  prdsbas2  17389  prdsplusgval  17393  prdsmulrval  17395  prdsleval  17397  prdsvscaval  17399  imasleval  17462  ssclem  17743  isssc  17744  rescval2  17752  issubc2  17760  cofuval  17806  resfval2  17817  resf1st  17818  resf2nd  17819  prdsmgp  20086  lspextmo  21008  dsmmfi  21693  ofco2  22395  neiss2  23045  txdis1cn  23579  qtopcld  23657  qtoprest  23661  kqsat  23675  kqdisj  23676  isr0  23681  elfm3  23894  ovolunlem1  25454  ofpreima  32743  ofpreima2  32744  fnpreimac  32749  fsuppcurry1  32803  fsuppcurry2  32804  pfxf1  33024  s2rnOLD  33026  s3rnOLD  33028  cycpmfvlem  33194  cycpmfv1  33195  cycpmfv2  33196  cycpmfv3  33197  1arithidomlem2  33617  1arithidom  33618  esplyind  33731  ply1annidllem  33858  ofcfval  34255  probfinmeasb  34585  bnj564  34900  bnj1121  35141  bnj1442  35205  bnj1450  35206  bnj1501  35223  fnrelpredd  35247  sdclem2  37939  prdstotbnd  37991  diadm  41291  dibdiadm  41411  dibdmN  41413  dicdmN  41440  dihdm  41525  aks4d1p1p5  42325  aks6d1c6lem2  42421  tfsconcat0b  43584  fnchoice  45270  wessf1ornlem  45425  limsupequzlem  45962  climrescn  45988  icccncfext  46127  stoweidlem35  46275  stoweidlem59  46299  smflimmpt  47050  smflimsuplem7  47066  iinfssclem1  49295  infsubc2d  49303  oppfvallem  49376  funcoppc3  49388  uptposlem  49438