Theorem fndmd 6603

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

Syntax hints:   → wi 4   = wceq 1542  dom cdm 5631   Fn wfn 6493

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 207  df-an 396  df-fn 6501

This theorem is referenced by:  fdm  6677  f1dm  6740  f1o00  6815  fvelimad  6907  rescnvimafod  7025  f1eqcocnv  7256  ofrfvalg  7639  offval  7640  fndmexd  7855  dmmpoga  8026  fnwelem  8081  frrlem4  8239  frrlem8  8243  frrlem10  8245  fpr2  8254  fprresex  8260  wfr2  8277  tfrlem5  8319  ixpiunwdom  9505  frr2  9684  dfac12lem1  10066  ackbij2lem3  10162  itunisuc  10341  ttukeylem3  10433  prdsbas2  17432  prdsplusgval  17436  prdsmulrval  17438  prdsleval  17440  prdsvscaval  17442  imasleval  17505  ssclem  17786  isssc  17787  rescval2  17795  issubc2  17803  cofuval  17849  resfval2  17860  resf1st  17861  resf2nd  17862  prdsmgp  20132  lspextmo  21051  dsmmfi  21718  ofco2  22416  neiss2  23066  txdis1cn  23600  qtopcld  23678  qtoprest  23682  kqsat  23696  kqdisj  23697  isr0  23702  elfm3  23915  ovolunlem1  25464  ofpreima  32738  ofpreima2  32739  fnpreimac  32743  fsuppcurry1  32797  fsuppcurry2  32798  pfxf1  33002  s2rnOLD  33004  s3rnOLD  33006  cycpmfvlem  33173  cycpmfv1  33174  cycpmfv2  33175  cycpmfv3  33176  1arithidomlem2  33596  1arithidom  33597  esplyind  33719  ply1annidllem  33845  ofcfval  34242  probfinmeasb  34572  bnj564  34887  bnj1121  35127  bnj1442  35191  bnj1450  35192  bnj1501  35209  fnrelpredd  35234  sdclem2  38063  prdstotbnd  38115  diadm  41481  dibdiadm  41601  dibdmN  41603  dicdmN  41630  dihdm  41715  aks4d1p1p5  42514  aks6d1c6lem2  42610  tfsconcat0b  43774  fnchoice  45460  wessf1ornlem  45615  limsupequzlem  46150  climrescn  46176  icccncfext  46315  stoweidlem35  46463  stoweidlem59  46487  smflimmpt  47238  smflimsuplem7  47254  iinfssclem1  49529  infsubc2d  49537  oppfvallem  49610  funcoppc3  49622  uptposlem  49672