Theorem fndmd 6645

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

This proof depends on syntax axioms:   → wi 4   = wceq 1569  dom cdm 5650   Fn wfn 6534

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 6542

This theorem is used by:  fdm  6720  f1dm  6785  f1odm  6829  f1o00  6861  fvelimad  6953  rescnvimafod  7074  f1eqcocnv  7310  ofrfvalg  7702  offval  7703  fndmexd  7917  dmmpoga  8087  fnwelem  8146  frrlem4  8311  frrlem8  8315  frrlem10  8317  fpr2  8326  fprresex  8332  wfr2  8349  tfrlem5  8391  ixpiunwdom  9588  frr2  9768  dfac12lem1  10226  ackbij2lem3  10322  itunisuc  10501  ttukeylem3  10593  prdsbas2  17646  prdsplusgval  17650  prdsmulrval  17652  prdsleval  17654  prdsvscaval  17656  imasleval  17719  ssclem  18000  isssc  18001  rescval2  18009  issubc2  18017  cofuval  18063  resfval2  18074  resf1st  18075  resf2nd  18076  prdsmgp  20377  lspextmo  21337  dsmmfi  22050  ofco2  22772  neiss2  23425  txdis1cn  23960  qtopcld  24038  qtoprest  24042  kqsat  24056  kqdisj  24057  isr0  24062  elfm3  24275  ovolunlem1  25824  ofpreima  33307  ofpreima2  33308  fnpreimac  33312  fsuppcurry1  33363  fsuppcurry2  33364  pfxf1  33556  cycpmfvlem  33720  cycpmfv1  33721  cycpmfv2  33722  cycpmfv3  33723  1arithidomlem2  34115  1arithidom  34116  esplyind  34254  ply1annidllem  34380  ofcfval  34777  probfinmeasb  35107  bnj564  35422  bnj1121  35662  bnj1442  35726  bnj1450  35727  bnj1501  35744  fnrelpredd  35773  onvfowev  35970  sdclem2  38770  prdstotbnd  38822  diadm  42186  dibdiadm  42306  dibdmN  42308  dicdmN  42335  dihdm  42420  aks4d1p1p5  43219  aks6d1c6lem2  43315  tfsconcat0b  44442  fnchoice  46140  wessf1ornlem  46294  limsupequzlem  46826  climrescn  46852  icccncfext  46991  stoweidlem35  47139  stoweidlem59  47163  smflimmpt  47914  smflimsuplem7  47930  iinfssclem1  50262  infsubc2d  50270  oppfvallem  50345  funcoppc3  50357  uptposlem  50407