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

Theorem ssexi 3923
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 3922 . 2  |-  ( A 
C_  B  ->  A  e.  _V )
41, 3ax-mp 7 1  |-  A  e. 
_V
Colors of variables: wff set class
Syntax hints:    e. wcel 1409   _Vcvv 2574    C_ wss 2945
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-io 640  ax-5 1352  ax-7 1353  ax-gen 1354  ax-ie1 1398  ax-ie2 1399  ax-8 1411  ax-10 1412  ax-11 1413  ax-i12 1414  ax-bndl 1415  ax-4 1416  ax-17 1435  ax-i9 1439  ax-ial 1443  ax-i5r 1444  ax-ext 2038  ax-sep 3903
This theorem depends on definitions:  df-bi 114  df-tru 1262  df-nf 1366  df-sb 1662  df-clab 2043  df-cleq 2049  df-clel 2052  df-nfc 2183  df-v 2576  df-in 2952  df-ss 2959
This theorem is referenced by:  zfausab  3927  pp0ex  3968  ord3ex  3969  epse  4107  opabex  5413  oprabex  5783  phplem2  6347  phpm  6358  niex  6468  enqex  6516  enq0ex  6595  npex  6629  ltnqex  6705  gtnqex  6706  recexprlemell  6778  recexprlemelu  6779  enrex  6880  axcnex  6993  peano5nnnn  7024  reex  7073  nnex  7996  zex  8311  qex  8664  ixxex  8869  frecuzrdgrrn  9358  frec2uzrdg  9359  frecuzrdgrom  9360  frecuzrdgsuc  9365  resqrexlemf  9834  resqrexlemf1  9835  resqrexlemfp1  9836  iserclim0  10057  climle  10085
  Copyright terms: Public domain W3C validator