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

Theorem elexi 2567
 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 2566 . 2 (𝐴𝐵𝐴 ∈ V)
31, 2ax-mp 7 1 𝐴 ∈ V
 Colors of variables: wff set class Syntax hints:   ∈ wcel 1393  Vcvv 2557 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1336  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-8 1395  ax-4 1400  ax-17 1419  ax-i9 1423  ax-ial 1427  ax-ext 2022 This theorem depends on definitions:  df-bi 110  df-sb 1646  df-clab 2027  df-cleq 2033  df-clel 2036  df-v 2559 This theorem is referenced by:  onunisuci  4169  ordsoexmid  4286  fnoei  6032  oeiexg  6033  endisj  6298  indpi  6440  prarloclemarch2  6517  prarloclemlt  6591  opelreal  6904  elreal  6905  elreal2  6907  eqresr  6912  c0ex  7021  1ex  7022  2ex  7987  3ex  7991  pnfex  8693  elxr  8696
 Copyright terms: Public domain W3C validator