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

Theorem elex 2624
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 1551 . 2 (∃𝑥(𝑥 = 𝐴𝑥𝐵) → ∃𝑥 𝑥 = 𝐴)
2 df-clel 2081 . 2 (𝐴𝐵 ↔ ∃𝑥(𝑥 = 𝐴𝑥𝐵))
3 isset 2619 . 2 (𝐴 ∈ V ↔ ∃𝑥 𝑥 = 𝐴)
41, 2, 33imtr4i 199 1 (𝐴𝐵𝐴 ∈ V)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 102   = wceq 1287  wex 1424  wcel 1436  Vcvv 2615
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1379  ax-gen 1381  ax-ie1 1425  ax-ie2 1426  ax-8 1438  ax-4 1443  ax-17 1462  ax-i9 1466  ax-ial 1470  ax-ext 2067
This theorem depends on definitions:  df-bi 115  df-sb 1690  df-clab 2072  df-cleq 2078  df-clel 2081  df-v 2617
This theorem is referenced by:  elexi  2625  elexd  2626  elisset  2627  vtoclgft  2663  vtoclgf  2671  vtocl2gf  2674  vtocl3gf  2675  spcimgft  2688  spcimegft  2690  elab4g  2755  elrabf  2760  mob  2788  sbcex  2837  sbcel1v  2890  sbcabel  2909  csbcomg  2943  csbvarg  2947  csbiebt  2956  csbnestgf  2969  csbidmg  2973  sbcco3g  2974  csbco3g  2975  eldif  2997  ssv  3035  elun  3130  elin  3172  snidb  3457  dfopg  3603  eluni  3639  eliun  3717  csbexga  3942  nvel  3947  class2seteq  3973  axpweq  3981  snelpwi  4013  opexg  4029  elopab  4059  epelg  4091  elon2  4177  unexg  4242  reuhypd  4267  sucexg  4288  sucelon  4293  onsucelsucr  4298  sucunielr  4300  en2lp  4343  peano2  4383  peano2b  4402  opelvvg  4455  opeliunxp  4461  opeliunxp2  4544  ideqg  4555  elrnmptg  4655  imasng  4764  iniseg  4771  opswapg  4883  elxp4  4884  elxp5  4885  dmmptg  4894  iota2  4972  fnmpt  5105  fvexg  5287  fvelimab  5323  mptfvex  5351  fvmptdf  5353  fvmptdv2  5355  mpteqb  5356  fvmptt  5357  fvmptf  5358  fvopab6  5359  fsn2  5434  fmptpr  5452  eloprabga  5692  ovmpt2s  5725  ov2gf  5726  ovmpt2dxf  5727  ovmpt2x  5730  ovmpt2ga  5731  ovmpt2df  5733  ovi3  5738  ovelrn  5750  suppssfv  5809  suppssov1  5810  offval3  5862  1stexg  5895  2ndexg  5896  elxp6  5897  elxp7  5898  releldm2  5912  fnmpt2  5929  mpt2fvex  5930  mpt2exg  5935  brtpos2  5970  rdgtfr  6093  rdgruledefgg  6094  frec0g  6116  sucinc2  6161  nntri3or  6208  relelec  6284  ecdmn0m  6286  mapvalg  6367  pmvalg  6368  elpmg  6373  map1  6481  mapdom1g  6515  mapxpen  6516  djulclr  6685  djurclr  6686  djulcl  6687  djurcl  6688  djulclb  6691  djuss  6705  1stinl  6709  2ndinl  6710  1stinr  6711  2ndinr  6712  elinp  6977  addnqprlemfl  7062  addnqprlemfu  7063  mulnqprlemfl  7078  mulnqprlemfu  7079  recexprlemell  7125  recexprlemelu  7126  ibcval5  10068  shftfvalg  10149  clim  10564  climmpt  10583  climshft2  10589  bj-vtoclgft  11120  djucllem  11145  bj-nvel  11233
  Copyright terms: Public domain W3C validator