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

Theorem elexi 2667
Description: If a class is a member of another class, it is a set. (Contributed by NM, 11-Jun-1994.)
Hypothesis
Ref Expression
elisseti.1  |-  A  e.  B
Assertion
Ref Expression
elexi  |-  A  e. 
_V

Proof of Theorem elexi
StepHypRef Expression
1 elisseti.1 . 2  |-  A  e.  B
2 elex 2666 . 2  |-  ( A  e.  B  ->  A  e.  _V )
31, 2ax-mp 7 1  |-  A  e. 
_V
Colors of variables: wff set class
Syntax hints:    e. wcel 1461   _Vcvv 2655
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1404  ax-gen 1406  ax-ie1 1450  ax-ie2 1451  ax-8 1463  ax-4 1468  ax-17 1487  ax-i9 1491  ax-ial 1495  ax-ext 2095
This theorem depends on definitions:  df-bi 116  df-sb 1717  df-clab 2100  df-cleq 2106  df-clel 2109  df-v 2657
This theorem is referenced by:  onunisuci  4312  ordsoexmid  4435  1oex  6273  fnoei  6300  oeiexg  6301  endisj  6669  unfiexmid  6757  snexxph  6788  djuex  6878  0ct  6942  infnninf  6970  nnnninf  6971  ctssexmid  6972  pm54.43  6993  prarloclemarch2  7169  opelreal  7556  elreal  7557  elreal2  7559  eqresr  7565  c0ex  7678  1ex  7679  pnfex  7737  sup3exmid  8619  2ex  8696  3ex  8700  elxr  9450  setsslid  11846  setsslnid  11847  0nninf  12878  nninfex  12886  nninffeq  12897
  Copyright terms: Public domain W3C validator