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

Theorem elex 2583
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 (𝐴𝐵𝐴 ∈ V)

Proof of Theorem elex
Dummy variable 𝑥 is distinct from all other variables.
StepHypRef Expression
1 exsimpl 1524 . 2 (∃𝑥(𝑥 = 𝐴𝑥𝐵) → ∃𝑥 𝑥 = 𝐴)
2 df-clel 2052 . 2 (𝐴𝐵 ↔ ∃𝑥(𝑥 = 𝐴𝑥𝐵))
3 isset 2578 . 2 (𝐴 ∈ V ↔ ∃𝑥 𝑥 = 𝐴)
41, 2, 33imtr4i 194 1 (𝐴𝐵𝐴 ∈ V)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 101   = wceq 1259  wex 1397  wcel 1409  Vcvv 2574
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-5 1352  ax-gen 1354  ax-ie1 1398  ax-ie2 1399  ax-8 1411  ax-4 1416  ax-17 1435  ax-i9 1439  ax-ial 1443  ax-ext 2038
This theorem depends on definitions:  df-bi 114  df-sb 1662  df-clab 2043  df-cleq 2049  df-clel 2052  df-v 2576
This theorem is referenced by:  elexi  2584  elisset  2585  vtoclgft  2621  vtoclgf  2629  vtocl2gf  2632  vtocl3gf  2633  spcimgft  2646  spcimegft  2648  elab4g  2713  elrabf  2718  mob  2745  sbcex  2794  sbcel1v  2847  sbcabel  2866  csbcomg  2900  csbvarg  2904  csbiebt  2913  csbnestgf  2925  csbidmg  2929  sbcco3g  2930  csbco3g  2931  eldif  2954  ssv  2992  elun  3111  elin  3153  snidb  3428  dfopg  3574  eluni  3610  eliun  3688  csbexga  3912  nvel  3916  class2seteq  3943  axpweq  3951  snelpwi  3975  prelpwi  3977  opexg  3991  elopab  4022  epelg  4054  elon2  4140  unexg  4205  reuhypd  4230  op1stbg  4237  sucexg  4251  sucelon  4256  onsucelsucr  4261  sucunielr  4263  en2lp  4305  peano2  4345  peano2b  4364  opelvvg  4416  opeliunxp  4422  opbrop  4446  opeliunxp2  4503  ideqg  4514  elrnmptg  4613  imasng  4717  iniseg  4724  opswapg  4834  elxp4  4835  elxp5  4836  dmmptg  4845  iota2  4920  fnmpt  5052  fvexg  5221  fvelimab  5256  mptfvex  5283  fvmptdf  5285  fvmptdv2  5287  mpteqb  5288  fvmptt  5289  fvmptf  5290  fvopab6  5291  fsn2  5364  fmptpr  5382  fliftel  5460  eloprabga  5618  ovmpt2s  5651  ov2gf  5652  ovmpt2dxf  5653  ovmpt2x  5656  ovmpt2ga  5657  ovmpt2df  5659  ovi3  5664  ovelrn  5676  suppssfv  5735  suppssov1  5736  offval3  5788  1stexg  5821  2ndexg  5822  elxp6  5823  elxp7  5824  releldm2  5838  fnmpt2  5855  mpt2fvex  5856  mpt2exg  5861  brtpos2  5896  rdgtfr  5991  rdgruledefgg  5992  frec0g  6013  sucinc2  6056  nntri3or  6102  relelec  6176  ecdmn0m  6178  elinp  6629  addnqprlemfl  6714  addnqprlemfu  6715  mulnqprlemfl  6730  mulnqprlemfu  6731  recexprlemell  6777  recexprlemelu  6778  ibcval5  9630  shftfvalg  9646  clim  10032  climmpt  10051  climshft2  10057  bj-vtoclgft  10287  bj-nvel  10390
  Copyright terms: Public domain W3C validator