Theorem fndmd 6636

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 6634	. 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 6526

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 6534

This theorem is used by:  fdm  6711  f1dm  6776  f1odm  6820  f1o00  6852  fvelimad  6944  rescnvimafod  7065  f1eqcocnv  7301  ofrfvalg  7690  offval  7691  fndmexd  7905  dmmpoga  8075  fnwelem  8132  frrlem4  8291  frrlem8  8295  frrlem10  8297  fpr2  8306  fprresex  8312  wfr2  8329  tfrlem5  8371  ixpiunwdom  9568  frr2  9748  dfac12lem1  10203  ackbij2lem3  10299  itunisuc  10478  ttukeylem3  10570  prdsbas2  17620  prdsplusgval  17624  prdsmulrval  17626  prdsleval  17628  prdsvscaval  17630  imasleval  17693  ssclem  17974  isssc  17975  rescval2  17983  issubc2  17991  cofuval  18037  resfval2  18048  resf1st  18049  resf2nd  18050  prdsmgp  20351  lspextmo  21311  dsmmfi  22024  ofco2  22746  neiss2  23399  txdis1cn  23934  qtopcld  24012  qtoprest  24016  kqsat  24030  kqdisj  24031  isr0  24036  elfm3  24249  ovolunlem1  25798  ofpreima  33241  ofpreima2  33242  fnpreimac  33246  fsuppcurry1  33298  fsuppcurry2  33299  pfxf1  33491  cycpmfvlem  33655  cycpmfv1  33656  cycpmfv2  33657  cycpmfv3  33658  1arithidomlem2  34050  1arithidom  34051  esplyind  34189  ply1annidllem  34315  ofcfval  34712  probfinmeasb  35043  bnj564  35358  bnj1121  35598  bnj1442  35662  bnj1450  35663  bnj1501  35680  fnrelpredd  35699  onvfowev  35868  sdclem2  38644  prdstotbnd  38696  diadm  42060  dibdiadm  42180  dibdmN  42182  dicdmN  42209  dihdm  42294  aks4d1p1p5  43093  aks6d1c6lem2  43189  tfsconcat0b  44306  fnchoice  45989  wessf1ornlem  46143  limsupequzlem  46676  climrescn  46702  icccncfext  46841  stoweidlem35  46989  stoweidlem59  47013  smflimmpt  47764  smflimsuplem7  47780  iinfssclem1  50106  infsubc2d  50114  oppfvallem  50187  funcoppc3  50199  uptposlem  50249