MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  resexd Structured version   Visualization version   GIF version

Theorem resexd 6048
Description: The restriction of a set is a set. (Contributed by Glauco Siliprandi, 23-Oct-2021.)
Hypothesis
Ref Expression
resexd.1 (𝜑𝐴𝑉)
Assertion
Ref Expression
resexd (𝜑 → (𝐴𝐵) ∈ V)

Proof of Theorem resexd
StepHypRef Expression
1 resexd.1 . 2 (𝜑𝐴𝑉)
2 resexg 6047 . 2 (𝐴𝑉 → (𝐴𝐵) ∈ V)
31, 2syl 17 1 (𝜑 → (𝐴𝐵) ∈ V)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2106  Vcvv 3478  cres 5691
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706  ax-sep 5302
This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1088  df-tru 1540  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-rab 3434  df-v 3480  df-in 3970  df-ss 3980  df-res 5701
This theorem is referenced by:  gsum2dlem2  20004  tsmspropd  24156  ulmss  26455  elrgspnlem4  33235  lmimdim  33631  aks6d1c6lem3  42154  psrbagres  42533  pwssplit4  43078  limsupresre  45652  limsupresico  45656  limsupresuz  45659  limsupres  45661  limsupresxr  45722  liminfresxr  45723  liminfresico  45727  liminfresre  45735  liminfresuz  45740  isubgriedg  47787  isubgrvtx  47791
  Copyright terms: Public domain W3C validator