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

Theorem elexi 2698
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 2697 . 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 1480   _Vcvv 2686
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 1423  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-4 1487  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-ext 2121
This theorem depends on definitions:  df-bi 116  df-sb 1736  df-clab 2126  df-cleq 2132  df-clel 2135  df-v 2688
This theorem is referenced by:  onunisuci  4357  ordsoexmid  4480  1oex  6324  fnoei  6351  oeiexg  6352  endisj  6721  unfiexmid  6809  snexxph  6841  djuex  6931  0ct  6995  infnninf  7025  nnnninf  7026  ctssexmid  7027  pm54.43  7058  prarloclemarch2  7246  opelreal  7654  elreal  7655  elreal2  7657  eqresr  7663  c0ex  7779  1ex  7780  pnfex  7838  sup3exmid  8734  2ex  8811  3ex  8815  elxr  9586  setsslid  12035  setsslnid  12036  subctctexmid  13342  0nninf  13345  nninfex  13353  nninffeq  13364
  Copyright terms: Public domain W3C validator