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

Theorem elexi 2670
 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 𝐴𝐵
Assertion
Ref Expression
elexi 𝐴 ∈ V

Proof of Theorem elexi
StepHypRef Expression
1 elisseti.1 . 2 𝐴𝐵
2 elex 2669 . 2 (𝐴𝐵𝐴 ∈ V)
31, 2ax-mp 5 1 𝐴 ∈ V
 Colors of variables: wff set class Syntax hints:   ∈ wcel 1463  Vcvv 2658 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 1406  ax-gen 1408  ax-ie1 1452  ax-ie2 1453  ax-8 1465  ax-4 1470  ax-17 1489  ax-i9 1493  ax-ial 1497  ax-ext 2097 This theorem depends on definitions:  df-bi 116  df-sb 1719  df-clab 2102  df-cleq 2108  df-clel 2111  df-v 2660 This theorem is referenced by:  onunisuci  4322  ordsoexmid  4445  1oex  6287  fnoei  6314  oeiexg  6315  endisj  6684  unfiexmid  6772  snexxph  6804  djuex  6894  0ct  6958  infnninf  6988  nnnninf  6989  ctssexmid  6990  pm54.43  7012  prarloclemarch2  7191  opelreal  7599  elreal  7600  elreal2  7602  eqresr  7608  c0ex  7724  1ex  7725  pnfex  7783  sup3exmid  8675  2ex  8752  3ex  8756  elxr  9514  setsslid  11915  setsslnid  11916  subctctexmid  13030  0nninf  13031  nninfex  13039  nninffeq  13050
 Copyright terms: Public domain W3C validator