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

Theorem elex 2700
Description: If a class is a member of another class, then 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 1597 . 2  |-  ( E. x ( x  =  A  /\  x  e.  B )  ->  E. x  x  =  A )
2 df-clel 2136 . 2  |-  ( A  e.  B  <->  E. x
( x  =  A  /\  x  e.  B
) )
3 isset 2695 . 2  |-  ( A  e.  _V  <->  E. x  x  =  A )
41, 2, 33imtr4i 200 1  |-  ( A  e.  B  ->  A  e.  _V )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 103    = wceq 1332   E.wex 1469    e. wcel 1481   _Vcvv 2689
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1424  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-4 1488  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-ext 2122
This theorem depends on definitions:  df-bi 116  df-sb 1737  df-clab 2127  df-cleq 2133  df-clel 2136  df-v 2691
This theorem is referenced by:  elexi  2701  elexd  2702  elisset  2703  vtoclgft  2739  vtoclgf  2747  vtoclg1f  2748  vtocl2gf  2751  vtocl3gf  2752  spcimgft  2765  spcimegft  2767  elab4g  2836  elrabf  2841  mob  2869  sbcex  2920  sbcel1v  2974  sbcabel  2993  csbcomg  3029  csbvarg  3034  csbiebt  3043  csbnestgf  3056  csbidmg  3060  sbcco3g  3061  csbco3g  3062  eldif  3084  ssv  3123  elun  3221  elin  3263  elpwb  3524  snidb  3561  dfopg  3710  eluni  3746  eliun  3824  csbexga  4063  nvel  4068  class2seteq  4094  axpweq  4102  snelpwi  4141  opexg  4157  elopab  4187  epelg  4219  elon2  4305  unexg  4371  reuhypd  4399  sucexg  4421  sucelon  4426  onsucelsucr  4431  sucunielr  4433  en2lp  4476  peano2  4516  peano2b  4535  opelvvg  4595  opeliunxp  4601  opeliunxp2  4686  ideqg  4697  elrnmptg  4798  imasng  4911  iniseg  4918  opswapg  5032  elxp4  5033  elxp5  5034  dmmptg  5043  iota2  5121  fnmpt  5256  fvexg  5447  fvelimab  5484  mptfvex  5513  fvmptdf  5515  fvmptdv2  5517  mpteqb  5518  fvmptt  5519  fvmptf  5520  fvopab6  5524  fsn2  5601  fmptpr  5619  eloprabga  5865  ovmpos  5901  ov2gf  5902  ovmpodxf  5903  ovmpox  5906  ovmpoga  5907  ovmpodf  5909  ovi3  5914  ovelrn  5926  suppssfv  5985  suppssov1  5986  offval3  6039  1stexg  6072  2ndexg  6073  elxp6  6074  elxp7  6075  releldm2  6090  fnmpo  6107  mpofvex  6108  mpoexg  6116  opeliunxp2f  6142  brtpos2  6155  rdgtfr  6278  rdgruledefgg  6279  frec0g  6301  sucinc2  6349  nntri3or  6396  relelec  6476  ecdmn0m  6478  mapvalg  6559  pmvalg  6560  elpmg  6565  elixp2  6603  mptelixpg  6635  elixpsn  6636  map1  6713  mapdom1g  6748  mapxpen  6749  fival  6865  elfi2  6867  djulclr  6941  djurclr  6942  djulcl  6943  djurcl  6944  djulclb  6947  inl11  6957  djuss  6962  1stinl  6966  2ndinl  6967  1stinr  6968  2ndinr  6969  ismkvnex  7036  omniwomnimkv  7048  cc4n  7102  elinp  7305  addnqprlemfl  7390  addnqprlemfu  7391  mulnqprlemfl  7406  mulnqprlemfu  7407  recexprlemell  7453  recexprlemelu  7454  shftfvalg  10621  clim  11081  climmpt  11100  climshft2  11106  isstruct2r  12007  slotex  12023  setsvalg  12026  setsfun0  12032  setscom  12036  restval  12163  topnvalg  12169  toponsspwpwg  12226  tgval  12255  eltg  12258  eltg2  12259  restbasg  12374  tgrest  12375  txvalex  12460  txval  12461  ispsmet  12529  ismet  12550  isxmet  12551  xmetunirn  12564  blfvalps  12591  bj-vtoclgft  13151  djucllem  13176  bj-nvel  13264
  Copyright terms: Public domain W3C validator