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

Theorem resexg 5349
Description: The restriction of a set is a set. (Contributed by NM, 28-Mar-1998.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)
Assertion
Ref Expression
resexg (𝐴𝑉 → (𝐴𝐵) ∈ V)

Proof of Theorem resexg
StepHypRef Expression
1 resss 5329 . 2 (𝐴𝐵) ⊆ 𝐴
2 ssexg 4727 . 2 (((𝐴𝐵) ⊆ 𝐴𝐴𝑉) → (𝐴𝐵) ∈ V)
31, 2mpan 701 1 (𝐴𝑉 → (𝐴𝐵) ∈ V)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 1976  Vcvv 3172  wss 3539  cres 5030
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589  ax-sep 4703
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-v 3174  df-in 3546  df-ss 3553  df-res 5040
This theorem is referenced by:  resex  5350  fvtresfn  6178  offres  7031  ressuppss  7178  ressuppssdif  7180  resixp  7806  fsuppres  8160  climres  14100  setsvalg  15665  setsid  15688  symgfixels  17623  gsumval3lem1  18075  gsumval3lem2  18076  gsum2dlem2  18139  qtopres  21253  tsmspropd  21687  ulmss  23872  uhgrares  25603  umgrares  25619  usgrares  25664  usgrares1  25705  cusgrares  25767  redwlk  25902  hhssva  27304  hhsssm  27305  hhshsslem1  27314  resf1o  28699  eulerpartlemmf  29570  exidres  32643  exidresid  32644  lmhmlnmsplit  36471  pwssplit4  36473  red1wlk  40876
  Copyright terms: Public domain W3C validator