Theorem fndmd 6591

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

Syntax hints:   → wi 4   = wceq 1540  dom cdm 5623   Fn wfn 6481

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 6489

This theorem is referenced by:  fdm  6665  f1dm  6728  f1o00  6803  fvelimad  6894  rescnvimafod  7011  f1eqcocnv  7242  ofrfvalg  7625  offval  7626  fndmexd  7844  dmmpoga  8015  fnwelem  8071  frrlem4  8229  frrlem8  8233  frrlem10  8235  fpr2  8244  fprresex  8250  wfr2  8267  tfrlem5  8309  ixpiunwdom  9501  frr2  9675  dfac12lem1  10057  ackbij2lem3  10153  itunisuc  10332  ttukeylem3  10424  prdsbas2  17391  prdsplusgval  17395  prdsmulrval  17397  prdsleval  17399  prdsvscaval  17401  imasleval  17463  ssclem  17744  isssc  17745  rescval2  17753  issubc2  17761  cofuval  17807  resfval2  17818  resf1st  17819  resf2nd  17820  prdsmgp  20054  lspextmo  20978  dsmmfi  21663  ofco2  22354  neiss2  23004  txdis1cn  23538  qtopcld  23616  qtoprest  23620  kqsat  23634  kqdisj  23635  isr0  23640  elfm3  23853  ovolunlem1  25414  ofpreima  32622  ofpreima2  32623  fnpreimac  32628  fsuppcurry1  32681  fsuppcurry2  32682  pfxf1  32896  s2rnOLD  32898  s3rnOLD  32900  cycpmfvlem  33067  cycpmfv1  33068  cycpmfv2  33069  cycpmfv3  33070  1arithidomlem2  33483  1arithidom  33484  ply1annidllem  33667  ofcfval  34064  probfinmeasb  34395  bnj564  34710  bnj1121  34951  bnj1442  35015  bnj1450  35016  bnj1501  35033  fnrelpredd  35055  sdclem2  37721  prdstotbnd  37773  diadm  41014  dibdiadm  41134  dibdmN  41136  dicdmN  41163  dihdm  41248  aks4d1p1p5  42048  aks6d1c6lem2  42144  tfsconcat0b  43319  fnchoice  45007  wessf1ornlem  45163  limsupequzlem  45704  climrescn  45730  icccncfext  45869  stoweidlem35  46017  stoweidlem59  46041  smflimmpt  46792  smflimsuplem7  46808  iinfssclem1  49040  infsubc2d  49048  oppfvallem  49121  funcoppc3  49133  uptposlem  49183