Theorem fndmd 6642

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

Syntax hints:   → wi 4   = wceq 1570  dom cdm 5663   Fn wfn 6533

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 210  df-an 401  df-fn 6541

This theorem is referenced by:  fdm  6717  f1dm  6782  f1odm  6826  f1o00  6858  fvelimad  6950  rescnvimafod  7070  f1eqcocnv  7301  ofrfvalg  7684  offval  7685  fndmexd  7902  dmmpoga  8071  fnwelem  8128  frrlem4  8287  frrlem8  8291  frrlem10  8293  fpr2  8302  fprresex  8308  wfr2  8325  tfrlem5  8367  ixpiunwdom  9553  frr2  9733  dfac12lem1  10128  ackbij2lem3  10224  itunisuc  10404  ttukeylem3  10496  prdsbas2  17523  prdsplusgval  17527  prdsmulrval  17529  prdsleval  17531  prdsvscaval  17533  imasleval  17596  ssclem  17877  isssc  17878  rescval2  17886  issubc2  17894  cofuval  17940  resfval2  17951  resf1st  17952  resf2nd  17953  prdsmgp  20228  lspextmo  21158  dsmmfi  21869  ofco2  22589  neiss2  23239  txdis1cn  23773  qtopcld  23851  qtoprest  23855  kqsat  23869  kqdisj  23870  isr0  23875  elfm3  24088  ovolunlem1  25637  ofpreima  32991  ofpreima2  32992  fnpreimac  32996  fsuppcurry1  33050  fsuppcurry2  33051  pfxf1  33243  s2rnOLD  33245  s3rnOLD  33247  cycpmfvlem  33413  cycpmfv1  33414  cycpmfv2  33415  cycpmfv3  33416  1arithidomlem2  33807  1arithidom  33808  esplyind  33946  ply1annidllem  34072  ofcfval  34469  probfinmeasb  34799  bnj564  35114  bnj1121  35354  bnj1442  35418  bnj1450  35419  bnj1501  35436  fnrelpredd  35463  onvfowev  35581  sdclem2  38374  prdstotbnd  38426  diadm  41790  dibdiadm  41910  dibdmN  41912  dicdmN  41939  dihdm  42024  aks4d1p1p5  42823  aks6d1c6lem2  42919  tfsconcat0b  44056  fnchoice  45732  wessf1ornlem  45886  limsupequzlem  46419  climrescn  46445  icccncfext  46584  stoweidlem35  46732  stoweidlem59  46756  smflimmpt  47507  smflimsuplem7  47523  iinfssclem1  49815  infsubc2d  49823  oppfvallem  49896  funcoppc3  49908  uptposlem  49958