Theorem fndmd 6647

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570  dom cdm 5666   Fn wfn 6538

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-fn 6546

This theorem is used by:  fdm  6722  f1dm  6787  f1odm  6831  f1o00  6863  fvelimad  6955  rescnvimafod  7075  f1eqcocnv  7310  ofrfvalg  7695  offval  7696  fndmexd  7910  dmmpoga  8079  fnwelem  8136  frrlem4  8295  frrlem8  8299  frrlem10  8301  fpr2  8310  fprresex  8316  wfr2  8333  tfrlem5  8375  ixpiunwdom  9562  frr2  9742  dfac12lem1  10146  ackbij2lem3  10242  itunisuc  10421  ttukeylem3  10513  prdsbas2  17547  prdsplusgval  17551  prdsmulrval  17553  prdsleval  17555  prdsvscaval  17557  imasleval  17620  ssclem  17901  isssc  17902  rescval2  17910  issubc2  17918  cofuval  17964  resfval2  17975  resf1st  17976  resf2nd  17977  prdsmgp  20258  lspextmo  21214  dsmmfi  21925  ofco2  22645  neiss2  23295  txdis1cn  23829  qtopcld  23907  qtoprest  23911  kqsat  23925  kqdisj  23926  isr0  23931  elfm3  24144  ovolunlem1  25693  ofpreima  33047  ofpreima2  33048  fnpreimac  33052  fsuppcurry1  33106  fsuppcurry2  33107  pfxf1  33299  cycpmfvlem  33463  cycpmfv1  33464  cycpmfv2  33465  cycpmfv3  33466  1arithidomlem2  33857  1arithidom  33858  esplyind  33996  ply1annidllem  34122  ofcfval  34519  probfinmeasb  34850  bnj564  35165  bnj1121  35405  bnj1442  35469  bnj1450  35470  bnj1501  35487  fnrelpredd  35507  onvfowev  35624  sdclem2  38434  prdstotbnd  38486  diadm  41850  dibdiadm  41970  dibdmN  41972  dicdmN  41999  dihdm  42084  aks4d1p1p5  42883  aks6d1c6lem2  42979  tfsconcat0b  44114  fnchoice  45790  wessf1ornlem  45944  limsupequzlem  46477  climrescn  46503  icccncfext  46642  stoweidlem35  46790  stoweidlem59  46814  smflimmpt  47565  smflimsuplem7  47581  iinfssclem1  49873  infsubc2d  49881  oppfvallem  49954  funcoppc3  49966  uptposlem  50016