Theorem fndmd 6623

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

Syntax hints:   → wi 4   = wceq 1540  dom cdm 5638   Fn wfn 6506

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 6514

This theorem is referenced by:  fdm  6697  f1dm  6760  f1o00  6835  fvelimad  6928  rescnvimafod  7045  f1eqcocnv  7276  ofrfvalg  7661  offval  7662  fndmexd  7880  dmmpoga  8052  fnwelem  8110  frrlem4  8268  frrlem8  8272  frrlem10  8274  fpr2  8283  fprresex  8289  wfr2  8306  tfrlem5  8348  ixpiunwdom  9543  frr2  9713  dfac12lem1  10097  ackbij2lem3  10193  itunisuc  10372  ttukeylem3  10464  prdsbas2  17432  prdsplusgval  17436  prdsmulrval  17438  prdsleval  17440  prdsvscaval  17442  imasleval  17504  ssclem  17781  isssc  17782  rescval2  17790  issubc2  17798  cofuval  17844  resfval2  17855  resf1st  17856  resf2nd  17857  prdsmgp  20060  lspextmo  20963  dsmmfi  21647  ofco2  22338  neiss2  22988  txdis1cn  23522  qtopcld  23600  qtoprest  23604  kqsat  23618  kqdisj  23619  isr0  23624  elfm3  23837  ovolunlem1  25398  ofpreima  32589  ofpreima2  32590  fnpreimac  32595  fsuppcurry1  32648  fsuppcurry2  32649  pfxf1  32863  s2rnOLD  32865  s3rnOLD  32867  cycpmfvlem  33069  cycpmfv1  33070  cycpmfv2  33071  cycpmfv3  33072  1arithidomlem2  33507  1arithidom  33508  ply1annidllem  33691  ofcfval  34088  probfinmeasb  34419  bnj564  34734  bnj1121  34975  bnj1442  35039  bnj1450  35040  bnj1501  35057  fnrelpredd  35079  sdclem2  37736  prdstotbnd  37788  diadm  41029  dibdiadm  41149  dibdmN  41151  dicdmN  41178  dihdm  41263  aks4d1p1p5  42063  aks6d1c6lem2  42159  tfsconcat0b  43335  fnchoice  45023  wessf1ornlem  45179  limsupequzlem  45720  climrescn  45746  icccncfext  45885  stoweidlem35  46033  stoweidlem59  46057  smflimmpt  46808  smflimsuplem7  46824  iinfssclem1  49043  infsubc2d  49051  oppfvallem  49124  funcoppc3  49136  uptposlem  49186