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

Theorem elexi 2612
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 2611 . 2 (𝐴𝐵𝐴 ∈ V)
31, 2ax-mp 7 1 𝐴 ∈ V
Colors of variables: wff set class
Syntax hints:  wcel 1434  Vcvv 2602
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1377  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-8 1436  ax-4 1441  ax-17 1460  ax-i9 1464  ax-ial 1468  ax-ext 2064
This theorem depends on definitions:  df-bi 115  df-sb 1687  df-clab 2069  df-cleq 2075  df-clel 2078  df-v 2604
This theorem is referenced by:  onunisuci  4189  ordsoexmid  4307  fnoei  6090  oeiexg  6091  1domsn  6353  endisj  6358  unfiexmid  6428  pm54.43  6508  indpi  6583  prarloclemarch2  6660  prarloclemlt  6734  opelreal  7047  elreal  7048  elreal2  7050  eqresr  7055  c0ex  7164  1ex  7165  pnfex  7223  2ex  8167  3ex  8171  elxr  8917
  Copyright terms: Public domain W3C validator