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

Theorem elex 2543
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 1490 . 2 (x(x = A x B) → x x = A)
2 df-clel 2018 . 2 (A Bx(x = A x B))
3 isset 2539 . 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   = wceq 1228  wex 1362   wcel 1374  Vcvv 2535
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 1376  ax-4 1381  ax-17 1400  ax-i9 1404  ax-ial 1409  ax-ext 2004
This theorem depends on definitions:  df-bi 110  df-sb 1628  df-clab 2009  df-cleq 2015  df-clel 2018  df-v 2537
This theorem is referenced by:  elexi  2544  elisset  2545  vtoclgft  2581  vtoclgf  2589  vtocl2gf  2592  vtocl3gf  2593  spcimgft  2606  spcimegft  2608  elab4g  2668  elrabf  2673  mob  2700  sbcex  2749  sbcabel  2816  csbcomg  2850  csbvarg  2854  csbiebt  2863  csbnestgf  2875  csbidmg  2879  sbcco3g  2880  csbco3g  2881  eldif  2904  ssv  2942  elun  3061  elin  3103  snidb  3376  dfopg  3521  eluni  3557  eliun  3635  csbexgOLD  3859  nvel  3863  class2seteq  3890  axpweq  3898  snelpwi  3922  prelpwi  3924  opexg  3938  elopab  3969  epelg  4001  elon2  4062  unexg  4128  reuhypd  4153  op1stbg  4160  sucexg  4174  sucelon  4179  onsucelsucr  4183  sucunielr  4185  en2lp  4216  peano2  4245  peano2b  4264  opelvvg  4316  opeliunxp  4322  opbrop  4346  opeliunxp2  4403  ideqg  4414  elrnmptg  4513  imasng  4617  iniseg  4624  opswapg  4734  elxp4  4735  elxp5  4736  dmmptg  4745  iota2  4820  fnmpt  4951  fvexg  5119  fvelimab  5154  mptfvex  5181  fvmptdf  5183  fvmptdv2  5185  mpteqb  5186  fvmptt  5187  fvmptf  5188  fvopab6  5189  fsn2  5262  fmptpr  5280  fliftel  5358  eloprabga  5514  ovmpt2s  5547  ov2gf  5548  ovmpt2dxf  5549  ovmpt2x  5552  ovmpt2ga  5553  ovmpt2df  5555  ovi3  5560  ovelrn  5572  suppssfv  5631  suppssov1  5632  offval3  5684  1stexg  5717  2ndexg  5718  elxp6  5719  elxp7  5720  releldm2  5734  fnmpt2  5751  mpt2fvex  5752  mpt2exg  5757  brtpos2  5788  rdgruledefgg  5882  sucinc2  5941  nntri3or  5987  relelec  6057  ecdmn0m  6059  elinp  6328  recexprlemell  6456  recexprlemelu  6457  bj-vtoclgft  7021  bj-nvel  7120
  Copyright terms: Public domain W3C validator