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 1570  dom cdm 5651   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  8144  frrlem4  8308  frrlem8  8312  frrlem10  8314  fpr2  8323  fprresex  8329  wfr2  8346  tfrlem5  8388  ixpiunwdom  9585  frr2  9765  dfac12lem1  10223  ackbij2lem3  10319  itunisuc  10498  ttukeylem3  10590  prdsbas2  17641  prdsplusgval  17645  prdsmulrval  17647  prdsleval  17649  prdsvscaval  17651  imasleval  17714  ssclem  17995  isssc  17996  rescval2  18004  issubc2  18012  cofuval  18058  resfval2  18069  resf1st  18070  resf2nd  18071  prdsmgp  20372  lspextmo  21332  dsmmfi  22045  ofco2  22767  neiss2  23420  txdis1cn  23955  qtopcld  24033  qtoprest  24037  kqsat  24051  kqdisj  24052  isr0  24057  elfm3  24270  ovolunlem1  25819  ofpreima  33260  ofpreima2  33261  fnpreimac  33265  fsuppcurry1  33317  fsuppcurry2  33318  pfxf1  33510  cycpmfvlem  33674  cycpmfv1  33675  cycpmfv2  33676  cycpmfv3  33677  1arithidomlem2  34069  1arithidom  34070  esplyind  34208  ply1annidllem  34334  ofcfval  34731  probfinmeasb  35061  bnj564  35376  bnj1121  35616  bnj1442  35680  bnj1450  35681  bnj1501  35698  fnrelpredd  35721  onvfowev  35900  sdclem2  38678  prdstotbnd  38730  diadm  42094  dibdiadm  42214  dibdmN  42216  dicdmN  42243  dihdm  42328  aks4d1p1p5  43127  aks6d1c6lem2  43223  tfsconcat0b  44349  fnchoice  46047  wessf1ornlem  46201  limsupequzlem  46733  climrescn  46759  icccncfext  46898  stoweidlem35  47046  stoweidlem59  47070  smflimmpt  47821  smflimsuplem7  47837  iinfssclem1  50163  infsubc2d  50171  oppfvallem  50244  funcoppc3  50256  uptposlem  50306