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

Theorem ssexi 4069
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 4068 . 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 1480   _Vcvv 2686    C_ wss 3071
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 698  ax-5 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-10 1483  ax-11 1484  ax-i12 1485  ax-bndl 1486  ax-4 1487  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2121  ax-sep 4049
This theorem depends on definitions:  df-bi 116  df-tru 1334  df-nf 1437  df-sb 1736  df-clab 2126  df-cleq 2132  df-clel 2135  df-nfc 2270  df-v 2688  df-in 3077  df-ss 3084
This theorem is referenced by:  zfausab  4073  pp0ex  4116  ord3ex  4117  epse  4267  opabex  5647  oprabex  6029  phplem2  6750  phpm  6762  snexxph  6841  sbthlem2  6849  niex  7139  enqex  7187  enq0ex  7266  npex  7300  ltnqex  7376  gtnqex  7377  recexprlemell  7449  recexprlemelu  7450  enrex  7564  axcnex  7686  peano5nnnn  7719  reex  7773  nnex  8745  zex  9082  qex  9446  ixxex  9705  iccen  9812  serclim0  11098  climle  11127  iserabs  11268  isumshft  11283  explecnv  11298  prodfclim1  11337  prmex  11817  exmidunben  11962  istopon  12206  dmtopon  12216  lmres  12443  climcncf  12766  reldvg  12843
  Copyright terms: Public domain W3C validator