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

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

Proof of Theorem elex
Dummy variable 𝑥 is distinct from all other variables.
StepHypRef Expression
1 exsimpl 1554 . 2 (∃𝑥(𝑥 = 𝐴𝑥𝐵) → ∃𝑥 𝑥 = 𝐴)
2 df-clel 2085 . 2 (𝐴𝐵 ↔ ∃𝑥(𝑥 = 𝐴𝑥𝐵))
3 isset 2626 . 2 (𝐴 ∈ V ↔ ∃𝑥 𝑥 = 𝐴)
41, 2, 33imtr4i 200 1 (𝐴𝐵𝐴 ∈ V)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103   = wceq 1290  wex 1427  wcel 1439  Vcvv 2620
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1382  ax-gen 1384  ax-ie1 1428  ax-ie2 1429  ax-8 1441  ax-4 1446  ax-17 1465  ax-i9 1469  ax-ial 1473  ax-ext 2071
This theorem depends on definitions:  df-bi 116  df-sb 1694  df-clab 2076  df-cleq 2082  df-clel 2085  df-v 2622
This theorem is referenced by:  elexi  2632  elexd  2633  elisset  2634  vtoclgft  2670  vtoclgf  2678  vtoclg1f  2679  vtocl2gf  2682  vtocl3gf  2683  spcimgft  2696  spcimegft  2698  elab4g  2765  elrabf  2770  mob  2798  sbcex  2849  sbcel1v  2902  sbcabel  2921  csbcomg  2955  csbvarg  2959  csbiebt  2968  csbnestgf  2981  csbidmg  2985  sbcco3g  2986  csbco3g  2987  eldif  3009  ssv  3047  elun  3142  elin  3184  elpwb  3443  snidb  3478  dfopg  3626  eluni  3662  eliun  3740  csbexga  3973  nvel  3978  class2seteq  4004  axpweq  4012  snelpwi  4048  opexg  4064  elopab  4094  epelg  4126  elon2  4212  unexg  4278  reuhypd  4306  sucexg  4328  sucelon  4333  onsucelsucr  4338  sucunielr  4340  en2lp  4383  peano2  4423  peano2b  4442  opelvvg  4500  opeliunxp  4506  opeliunxp2  4589  ideqg  4600  elrnmptg  4700  imasng  4810  iniseg  4817  opswapg  4930  elxp4  4931  elxp5  4932  dmmptg  4941  iota2  5019  fnmpt  5153  fvexg  5337  fvelimab  5373  mptfvex  5401  fvmptdf  5403  fvmptdv2  5405  mpteqb  5406  fvmptt  5407  fvmptf  5408  fvopab6  5410  fsn2  5485  fmptpr  5503  eloprabga  5749  ovmpt2s  5782  ov2gf  5783  ovmpt2dxf  5784  ovmpt2x  5787  ovmpt2ga  5788  ovmpt2df  5790  ovi3  5795  ovelrn  5807  suppssfv  5866  suppssov1  5867  offval3  5919  1stexg  5952  2ndexg  5953  elxp6  5954  elxp7  5955  releldm2  5969  fnmpt2  5986  mpt2fvex  5987  mpt2exg  5992  opeliunxp2f  6017  brtpos2  6030  rdgtfr  6153  rdgruledefgg  6154  frec0g  6176  sucinc2  6221  nntri3or  6268  relelec  6346  ecdmn0m  6348  mapvalg  6429  pmvalg  6430  elpmg  6435  elixp2  6473  mptelixpg  6505  elixpsn  6506  map1  6583  mapdom1g  6617  mapxpen  6618  djulclr  6795  djurclr  6796  djulcl  6797  djurcl  6798  djulclb  6801  djuss  6815  1stinl  6819  2ndinl  6820  1stinr  6821  2ndinr  6822  elinp  7087  addnqprlemfl  7172  addnqprlemfu  7173  mulnqprlemfl  7188  mulnqprlemfu  7189  recexprlemell  7235  recexprlemelu  7236  ibcval5  10225  shftfvalg  10306  clim  10723  climmpt  10742  climshft2  10749  isstruct2r  11559  slotex  11575  setsvalg  11578  setsfun0  11584  setscom  11588  restval  11712  topnvalg  11718  toponsspwpwg  11774  tgval  11803  eltg  11806  eltg2  11807  bj-vtoclgft  11941  djucllem  11966  bj-nvel  12054
  Copyright terms: Public domain W3C validator