ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  ssexi Unicode version

Theorem ssexi 4036
Description: The subset of a set is also a set. (Contributed by NM, 9-Sep-1993.)
Hypotheses
Ref Expression
ssexi.1  |-  B  e. 
_V
ssexi.2  |-  A  C_  B
Assertion
Ref Expression
ssexi  |-  A  e. 
_V

Proof of Theorem ssexi
StepHypRef Expression
1 ssexi.2 . 2  |-  A  C_  B
2 ssexi.1 . . 3  |-  B  e. 
_V
32ssex 4035 . 2  |-  ( A 
C_  B  ->  A  e.  _V )
41, 3ax-mp 5 1  |-  A  e. 
_V
Colors of variables: wff set class
Syntax hints:    e. wcel 1465   _Vcvv 2660    C_ wss 3041
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 683  ax-5 1408  ax-7 1409  ax-gen 1410  ax-ie1 1454  ax-ie2 1455  ax-8 1467  ax-10 1468  ax-11 1469  ax-i12 1470  ax-bndl 1471  ax-4 1472  ax-17 1491  ax-i9 1495  ax-ial 1499  ax-i5r 1500  ax-ext 2099  ax-sep 4016
This theorem depends on definitions:  df-bi 116  df-tru 1319  df-nf 1422  df-sb 1721  df-clab 2104  df-cleq 2110  df-clel 2113  df-nfc 2247  df-v 2662  df-in 3047  df-ss 3054
This theorem is referenced by:  zfausab  4040  pp0ex  4083  ord3ex  4084  epse  4234  opabex  5612  oprabex  5994  phplem2  6715  phpm  6727  snexxph  6806  sbthlem2  6814  niex  7088  enqex  7136  enq0ex  7215  npex  7249  ltnqex  7325  gtnqex  7326  recexprlemell  7398  recexprlemelu  7399  enrex  7513  axcnex  7635  peano5nnnn  7668  reex  7722  nnex  8694  zex  9031  qex  9392  ixxex  9650  serclim0  11042  climle  11071  iserabs  11212  isumshft  11227  explecnv  11242  prmex  11721  exmidunben  11866  istopon  12107  dmtopon  12117  lmres  12344  climcncf  12667  reldvg  12744
  Copyright terms: Public domain W3C validator