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

Theorem resexd 6046
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 6045 . 2 (𝐴𝑉 → (𝐴𝐵) ∈ V)
31, 2syl 17 1 (𝜑 → (𝐴𝐵) ∈ V)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2108  Vcvv 3480  cres 5687
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708  ax-sep 5296
This theorem depends on definitions:  df-bi 207  df-an 396  df-3an 1089  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-rab 3437  df-v 3482  df-in 3958  df-ss 3968  df-res 5697
This theorem is referenced by:  gsum2dlem2  19989  tsmspropd  24140  ulmss  26440  elrgspnlem4  33249  lmimdim  33654  aks6d1c6lem3  42173  psrbagres  42556  pwssplit4  43101  limsupresre  45711  limsupresico  45715  limsupresuz  45718  limsupres  45720  limsupresxr  45781  liminfresxr  45782  liminfresico  45786  liminfresre  45794  liminfresuz  45799  isubgriedg  47849  isubgrvtx  47853
  Copyright terms: Public domain W3C validator