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

Theorem elexi 2672
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 2671 . 2  |-  ( A  e.  B  ->  A  e.  _V )
31, 2ax-mp 5 1  |-  A  e. 
_V
Colors of variables: wff set class
Syntax hints:    e. wcel 1465   _Vcvv 2660
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-5 1408  ax-gen 1410  ax-ie1 1454  ax-ie2 1455  ax-8 1467  ax-4 1472  ax-17 1491  ax-i9 1495  ax-ial 1499  ax-ext 2099
This theorem depends on definitions:  df-bi 116  df-sb 1721  df-clab 2104  df-cleq 2110  df-clel 2113  df-v 2662
This theorem is referenced by:  onunisuci  4324  ordsoexmid  4447  1oex  6289  fnoei  6316  oeiexg  6317  endisj  6686  unfiexmid  6774  snexxph  6806  djuex  6896  0ct  6960  infnninf  6990  nnnninf  6991  ctssexmid  6992  pm54.43  7014  prarloclemarch2  7195  opelreal  7603  elreal  7604  elreal2  7606  eqresr  7612  c0ex  7728  1ex  7729  pnfex  7787  sup3exmid  8683  2ex  8760  3ex  8764  elxr  9531  setsslid  11936  setsslnid  11937  subctctexmid  13123  0nninf  13124  nninfex  13132  nninffeq  13143
  Copyright terms: Public domain W3C validator