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

Theorem resexg 5582
 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 5562 . 2 (𝐴𝐵) ⊆ 𝐴
2 ssexg 4939 . 2 (((𝐴𝐵) ⊆ 𝐴𝐴𝑉) → (𝐴𝐵) ∈ V)
31, 2mpan 670 1 (𝐴𝑉 → (𝐴𝐵) ∈ V)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∈ wcel 2145  Vcvv 3351   ⊆ wss 3723   ↾ cres 5252 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-sep 4916 This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-v 3353  df-in 3730  df-ss 3737  df-res 5262 This theorem is referenced by:  resex  5583  fvtresfn  6428  offres  7314  ressuppss  7469  ressuppssdif  7471  resixp  8101  fsuppres  8460  climres  14514  setsvalg  16094  setsid  16121  symgfixels  18061  gsumval3lem1  18513  gsumval3lem2  18514  gsum2dlem2  18577  qtopres  21722  tsmspropd  22155  ulmss  24371  vtxdginducedm1  26674  redwlk  26804  hhssva  28454  hhsssm  28455  hhshsslem1  28464  resf1o  29845  eulerpartlemmf  30777  exidres  34009  exidresid  34010  xrnresex  34506  lmhmlnmsplit  38183  pwssplit4  38185  resexd  39841  setsv  41873
 Copyright terms: Public domain W3C validator