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

Theorem elexi 2749
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 2748 . 2 (𝐴𝐵𝐴 ∈ V)
31, 2ax-mp 5 1 𝐴 ∈ V
Colors of variables: wff set class
Syntax hints:  wcel 2148  Vcvv 2737
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1447  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-ext 2159
This theorem depends on definitions:  df-bi 117  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-v 2739
This theorem is referenced by:  elpwi2  4155  onunisuci  4429  ordsoexmid  4558  1oex  6419  fnoei  6447  oeiexg  6448  endisj  6818  unfiexmid  6911  snexxph  6943  djuex  7036  0ct  7100  nninfex  7114  infnninfOLD  7117  nnnninf  7118  ctssexmid  7142  nninfdcinf  7163  nninfwlporlem  7165  nninfwlpoimlemg  7167  pm54.43  7183  pw1ne3  7223  3nsssucpw1  7229  2omotaplemst  7248  prarloclemarch2  7409  opelreal  7817  elreal  7818  elreal2  7820  eqresr  7826  c0ex  7942  1ex  7943  pnfex  8001  sup3exmid  8903  2ex  8980  3ex  8984  elxr  9763  setsslid  12495  setsslnid  12496  lgsdir2lem3  14098  subctctexmid  14406  0nninf  14409  nninffeq  14425
  Copyright terms: Public domain W3C validator