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

Theorem elex 2697
 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 1596 . 2 (∃𝑥(𝑥 = 𝐴𝑥𝐵) → ∃𝑥 𝑥 = 𝐴)
2 df-clel 2135 . 2 (𝐴𝐵 ↔ ∃𝑥(𝑥 = 𝐴𝑥𝐵))
3 isset 2692 . 2 (𝐴 ∈ V ↔ ∃𝑥 𝑥 = 𝐴)
41, 2, 33imtr4i 200 1 (𝐴𝐵𝐴 ∈ V)
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 103   = wceq 1331  ∃wex 1468   ∈ wcel 1480  Vcvv 2686 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 1423  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-4 1487  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-ext 2121 This theorem depends on definitions:  df-bi 116  df-sb 1736  df-clab 2126  df-cleq 2132  df-clel 2135  df-v 2688 This theorem is referenced by:  elexi  2698  elexd  2699  elisset  2700  vtoclgft  2736  vtoclgf  2744  vtoclg1f  2745  vtocl2gf  2748  vtocl3gf  2749  spcimgft  2762  spcimegft  2764  elab4g  2833  elrabf  2838  mob  2866  sbcex  2917  sbcel1v  2971  sbcabel  2990  csbcomg  3025  csbvarg  3030  csbiebt  3039  csbnestgf  3052  csbidmg  3056  sbcco3g  3057  csbco3g  3058  eldif  3080  ssv  3119  elun  3217  elin  3259  elpwb  3520  snidb  3555  dfopg  3703  eluni  3739  eliun  3817  csbexga  4056  nvel  4061  class2seteq  4087  axpweq  4095  snelpwi  4134  opexg  4150  elopab  4180  epelg  4212  elon2  4298  unexg  4364  reuhypd  4392  sucexg  4414  sucelon  4419  onsucelsucr  4424  sucunielr  4426  en2lp  4469  peano2  4509  peano2b  4528  opelvvg  4588  opeliunxp  4594  opeliunxp2  4679  ideqg  4690  elrnmptg  4791  imasng  4904  iniseg  4911  opswapg  5025  elxp4  5026  elxp5  5027  dmmptg  5036  iota2  5114  fnmpt  5249  fvexg  5440  fvelimab  5477  mptfvex  5506  fvmptdf  5508  fvmptdv2  5510  mpteqb  5511  fvmptt  5512  fvmptf  5513  fvopab6  5517  fsn2  5594  fmptpr  5612  eloprabga  5858  ovmpos  5894  ov2gf  5895  ovmpodxf  5896  ovmpox  5899  ovmpoga  5900  ovmpodf  5902  ovi3  5907  ovelrn  5919  suppssfv  5978  suppssov1  5979  offval3  6032  1stexg  6065  2ndexg  6066  elxp6  6067  elxp7  6068  releldm2  6083  fnmpo  6100  mpofvex  6101  mpoexg  6109  opeliunxp2f  6135  brtpos2  6148  rdgtfr  6271  rdgruledefgg  6272  frec0g  6294  sucinc2  6342  nntri3or  6389  relelec  6469  ecdmn0m  6471  mapvalg  6552  pmvalg  6553  elpmg  6558  elixp2  6596  mptelixpg  6628  elixpsn  6629  map1  6706  mapdom1g  6741  mapxpen  6742  fival  6858  elfi2  6860  djulclr  6934  djurclr  6935  djulcl  6936  djurcl  6937  djulclb  6940  inl11  6950  djuss  6955  1stinl  6959  2ndinl  6960  1stinr  6961  2ndinr  6962  ismkvnex  7029  cc4n  7086  elinp  7289  addnqprlemfl  7374  addnqprlemfu  7375  mulnqprlemfl  7390  mulnqprlemfu  7391  recexprlemell  7437  recexprlemelu  7438  shftfvalg  10597  clim  11057  climmpt  11076  climshft2  11082  isstruct2r  11980  slotex  11996  setsvalg  11999  setsfun0  12005  setscom  12009  restval  12136  topnvalg  12142  toponsspwpwg  12199  tgval  12228  eltg  12231  eltg2  12232  restbasg  12347  tgrest  12348  txvalex  12433  txval  12434  ispsmet  12502  ismet  12523  isxmet  12524  xmetunirn  12537  blfvalps  12564  bj-vtoclgft  13012  djucllem  13037  bj-nvel  13125
 Copyright terms: Public domain W3C validator