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

Theorem elex 2563
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 1508 . 2 (∃𝑥(𝑥 = 𝐴𝑥𝐵) → ∃𝑥 𝑥 = 𝐴)
2 df-clel 2036 . 2 (𝐴𝐵 ↔ ∃𝑥(𝑥 = 𝐴𝑥𝐵))
3 isset 2558 . 2 (𝐴 ∈ V ↔ ∃𝑥 𝑥 = 𝐴)
41, 2, 33imtr4i 190 1 (𝐴𝐵𝐴 ∈ V)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 97   = wceq 1243  wex 1381  wcel 1393  Vcvv 2554
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 1336  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-8 1395  ax-4 1400  ax-17 1419  ax-i9 1423  ax-ial 1427  ax-ext 2022
This theorem depends on definitions:  df-bi 110  df-sb 1646  df-clab 2027  df-cleq 2033  df-clel 2036  df-v 2556
This theorem is referenced by:  elexi  2564  elisset  2565  vtoclgft  2601  vtoclgf  2609  vtocl2gf  2612  vtocl3gf  2613  spcimgft  2626  spcimegft  2628  elab4g  2688  elrabf  2693  mob  2720  sbcex  2769  sbcabel  2836  csbcomg  2870  csbvarg  2874  csbiebt  2883  csbnestgf  2895  csbidmg  2899  sbcco3g  2900  csbco3g  2901  eldif  2924  ssv  2962  elun  3081  elin  3123  snidb  3398  dfopg  3544  eluni  3580  eliun  3658  csbexga  3882  nvel  3886  class2seteq  3913  axpweq  3921  snelpwi  3945  prelpwi  3947  opexg  3961  elopab  3992  epelg  4024  elon2  4100  unexg  4165  reuhypd  4190  op1stbg  4197  sucexg  4211  sucelon  4216  onsucelsucr  4221  sucunielr  4223  en2lp  4263  peano2  4296  peano2b  4315  opelvvg  4367  opeliunxp  4373  opbrop  4397  opeliunxp2  4454  ideqg  4465  elrnmptg  4564  imasng  4668  iniseg  4675  opswapg  4785  elxp4  4786  elxp5  4787  dmmptg  4796  iota2  4871  fnmpt  5003  fvexg  5172  fvelimab  5207  mptfvex  5234  fvmptdf  5236  fvmptdv2  5238  mpteqb  5239  fvmptt  5240  fvmptf  5241  fvopab6  5242  fsn2  5315  fmptpr  5333  fliftel  5411  eloprabga  5569  ovmpt2s  5602  ov2gf  5603  ovmpt2dxf  5604  ovmpt2x  5607  ovmpt2ga  5608  ovmpt2df  5610  ovi3  5615  ovelrn  5627  suppssfv  5686  suppssov1  5687  offval3  5739  1stexg  5772  2ndexg  5773  elxp6  5774  elxp7  5775  releldm2  5789  fnmpt2  5806  mpt2fvex  5807  mpt2exg  5812  brtpos2  5844  rdgtfr  5939  rdgruledefgg  5940  frec0g  5961  sucinc2  6004  nntri3or  6050  relelec  6124  ecdmn0m  6126  elinp  6544  addnqprlemfl  6629  addnqprlemfu  6630  mulnqprlemfl  6645  mulnqprlemfu  6646  recexprlemell  6692  recexprlemelu  6693  shftfvalg  9288  clim  9670  climmpt  9689  climshft2  9695  bj-vtoclgft  9778  bj-nvel  9881
  Copyright terms: Public domain W3C validator