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

Theorem elex 2611
Description: If a class is a member of another class, it is a set. Theorem 6.12 of [Quine] p. 44. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 8-Jun-2011.)
Assertion
Ref Expression
elex  |-  ( A  e.  B  ->  A  e.  _V )

Proof of Theorem elex
Dummy variable  x is distinct from all other variables.
StepHypRef Expression
1 exsimpl 1549 . 2  |-  ( E. x ( x  =  A  /\  x  e.  B )  ->  E. x  x  =  A )
2 df-clel 2078 . 2  |-  ( A  e.  B  <->  E. x
( x  =  A  /\  x  e.  B
) )
3 isset 2606 . 2  |-  ( A  e.  _V  <->  E. x  x  =  A )
41, 2, 33imtr4i 199 1  |-  ( A  e.  B  ->  A  e.  _V )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 102    = wceq 1285   E.wex 1422    e. 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:  elexi  2612  elexd  2613  elisset  2614  vtoclgft  2650  vtoclgf  2658  vtocl2gf  2661  vtocl3gf  2662  spcimgft  2675  spcimegft  2677  elab4g  2743  elrabf  2748  mob  2775  sbcex  2824  sbcel1v  2877  sbcabel  2896  csbcomg  2930  csbvarg  2934  csbiebt  2943  csbnestgf  2955  csbidmg  2959  sbcco3g  2960  csbco3g  2961  eldif  2983  ssv  3020  elun  3114  elin  3156  snidb  3432  dfopg  3576  eluni  3612  eliun  3690  csbexga  3914  nvel  3918  class2seteq  3945  axpweq  3953  snelpwi  3975  opexg  3991  elopab  4021  epelg  4053  elon2  4139  unexg  4204  reuhypd  4229  sucexg  4250  sucelon  4255  onsucelsucr  4260  sucunielr  4262  en2lp  4305  peano2  4344  peano2b  4363  opelvvg  4415  opeliunxp  4421  opeliunxp2  4504  ideqg  4515  elrnmptg  4614  imasng  4720  iniseg  4727  opswapg  4837  elxp4  4838  elxp5  4839  dmmptg  4848  iota2  4923  fnmpt  5056  fvexg  5225  fvelimab  5261  mptfvex  5288  fvmptdf  5290  fvmptdv2  5292  mpteqb  5293  fvmptt  5294  fvmptf  5295  fvopab6  5296  fsn2  5369  fmptpr  5387  eloprabga  5622  ovmpt2s  5655  ov2gf  5656  ovmpt2dxf  5657  ovmpt2x  5660  ovmpt2ga  5661  ovmpt2df  5663  ovi3  5668  ovelrn  5680  suppssfv  5739  suppssov1  5740  offval3  5792  1stexg  5825  2ndexg  5826  elxp6  5827  elxp7  5828  releldm2  5842  fnmpt2  5859  mpt2fvex  5860  mpt2exg  5865  brtpos2  5900  rdgtfr  6023  rdgruledefgg  6024  frec0g  6046  sucinc2  6090  nntri3or  6137  relelec  6212  ecdmn0m  6214  elinp  6726  addnqprlemfl  6811  addnqprlemfu  6812  mulnqprlemfl  6827  mulnqprlemfu  6828  recexprlemell  6874  recexprlemelu  6875  ibcval5  9787  shftfvalg  9844  clim  10258  climmpt  10277  climshft2  10283  bj-vtoclgft  10736  bj-nvel  10846
  Copyright terms: Public domain W3C validator