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

Theorem elex 2542
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 BA V)

Proof of Theorem elex
Dummy variable x is distinct from all other variables.
StepHypRef Expression
1 exsimpl 1492 . 2 (x(x = A x B) → x x = A)
2 df-clel 2019 . 2 (A Bx(x = A x B))
3 isset 2538 . 2 (A V ↔ x x = A)
41, 2, 33imtr4i 190 1 (A BA V)
Colors of variables: wff set class
Syntax hints:  wi 4   wa 97  wex 1362   = wceq 1374   wcel 1376  Vcvv 2534
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 1316  ax-gen 1318  ax-ie1 1363  ax-ie2 1364  ax-8 1378  ax-4 1383  ax-17 1402  ax-i9 1406  ax-ial 1411  ax-ext 2005
This theorem depends on definitions:  df-bi 110  df-sb 1629  df-clab 2010  df-cleq 2016  df-clel 2019  df-v 2536
This theorem is referenced by:  elexi  2543  elisset  2544  vtoclgft  2580  vtoclgf  2588  vtocl2gf  2591  vtocl3gf  2592  spcimgft  2605  spcimegft  2607  elab4g  2667  elrabf  2672  mob  2699  sbcex  2748  sbcabel  2816  csbcomg  2850  csbvarg  2854  csbiebt  2863  csbnestgf  2875  csbidmg  2880  sbcco3g  2881  csbco3g  2883  eldif  2906  ssv  2944  elun  3063  elin  3105  snidb  3354  dfopg  3500  eluni  3536  eliun  3614  csbexgOLD  3838  nvel  3842  class2seteq  3869  axpweq  3877  snelpwi  3901  prelpwi  3903  opexg  3917  elopab  3948  epelg  3981  elon2  4038  unexg  4104  reuhypd  4129  op1stbg  4136  sucexg  4150  sucelon  4155  onsucelsucr  4159  sucunielr  4161  en2lp  4192  peano2  4221  peano2b  4240  opelvvg  4292  opeliunxp  4298  opbrop  4322  opeliunxp2  4379  ideqg  4390  elrnmptg  4489  imasng  4594  iniseg  4601  opswapg  4711  elxp4  4712  elxp5  4713  dmmptg  4722  iota2  4797  fnmpt  4928  fvexg  5096  fvelimab  5131  mptfvex  5158  fvmptdf  5160  fvmptdv2  5162  mpteqb  5163  fvmptt  5164  fvmptf  5165  fvopab6  5166  fsn2  5239  fmptpr  5257  fliftel  5335  eloprabga  5493  ovmpt2s  5526  ov2gf  5527  ovmpt2dxf  5528  ovmpt2x  5531  ovmpt2ga  5532  ovmpt2df  5534  ovelrn  5551  suppssfv  5607  suppssov1  5608  offval3  5660  1stexg  5693  2ndexg  5694  elxp6  5695  elxp7  5696  releldm2  5710  fnmpt2  5727  mpt2fvex  5728  mpt2exg  5733  brtpos2  5764  rdgruledefgg  5857  sucinc2  5916  nntri3or  5961  relelec  6028  ecdmn0m  6030
  Copyright terms: Public domain W3C validator