Theorem elex 2630

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	|- ( A e. B -> A e. _V )

Proof of Theorem elex

Dummy variable x is distinct from all other variables.

Step	Hyp	Ref	Expression
1		exsimpl 1553	. 2 |- ( E. x ( x = A /\ x e. B ) -> E. x x = A )
2		df-clel 2084	. 2 |- ( A e. B <-> E. x ( x = A /\ x e. B ) )
3		isset 2625	. 2 |- ( A e. _V <-> E. x x = A )
4	1, 2, 3	3imtr4i 199	1 |- ( A e. B -> A e. _V )

Syntax hints:   -> wi 4   /\ wa 102   = wceq 1289   E.wex 1426   e. wcel 1438   _Vcvv 2619

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 1381  ax-gen 1383  ax-ie1 1427  ax-ie2 1428  ax-8 1440  ax-4 1445  ax-17 1464  ax-i9 1468  ax-ial 1472  ax-ext 2070

This theorem depends on definitions:  df-bi 115  df-sb 1693  df-clab 2075  df-cleq 2081  df-clel 2084  df-v 2621

This theorem is referenced by:  elexi  2631  elexd  2632  elisset  2633  vtoclgft  2669  vtoclgf  2677  vtoclg1f  2678  vtocl2gf  2681  vtocl3gf  2682  spcimgft  2695  spcimegft  2697  elab4g  2762  elrabf  2767  mob  2795  sbcex  2846  sbcel1v  2899  sbcabel  2918  csbcomg  2952  csbvarg  2956  csbiebt  2965  csbnestgf  2978  csbidmg  2982  sbcco3g  2983  csbco3g  2984  eldif  3006  ssv  3044  elun  3139  elin  3181  snidb  3469  dfopg  3615  eluni  3651  eliun  3729  csbexga  3959  nvel  3964  class2seteq  3990  axpweq  3998  snelpwi  4030  opexg  4046  elopab  4076  epelg  4108  elon2  4194  unexg  4259  reuhypd  4284  sucexg  4305  sucelon  4310  onsucelsucr  4315  sucunielr  4317  en2lp  4360  peano2  4400  peano2b  4419  opelvvg  4475  opeliunxp  4481  opeliunxp2  4564  ideqg  4575  elrnmptg  4675  imasng  4784  iniseg  4791  opswapg  4904  elxp4  4905  elxp5  4906  dmmptg  4915  iota2  4993  fnmpt  5126  fvexg  5308  fvelimab  5344  mptfvex  5372  fvmptdf  5374  fvmptdv2  5376  mpteqb  5377  fvmptt  5378  fvmptf  5379  fvopab6  5380  fsn2  5455  fmptpr  5473  eloprabga  5717  ovmpt2s  5750  ov2gf  5751  ovmpt2dxf  5752  ovmpt2x  5755  ovmpt2ga  5756  ovmpt2df  5758  ovi3  5763  ovelrn  5775  suppssfv  5834  suppssov1  5835  offval3  5887  1stexg  5920  2ndexg  5921  elxp6  5922  elxp7  5923  releldm2  5937  fnmpt2  5954  mpt2fvex  5955  mpt2exg  5960  opeliunxp2f  5985  brtpos2  5998  rdgtfr  6121  rdgruledefgg  6122  frec0g  6144  sucinc2  6189  nntri3or  6236  relelec  6312  ecdmn0m  6314  mapvalg  6395  pmvalg  6396  elpmg  6401  map1  6509  mapdom1g  6543  mapxpen  6544  djulclr  6720  djurclr  6721  djulcl  6722  djurcl  6723  djulclb  6726  djuss  6740  1stinl  6744  2ndinl  6745  1stinr  6746  2ndinr  6747  elinp  7012  addnqprlemfl  7097  addnqprlemfu  7098  mulnqprlemfl  7113  mulnqprlemfu  7114  recexprlemell  7160  recexprlemelu  7161  ibcval5  10136  shftfvalg  10217  clim  10633  climmpt  10652  climshft2  10659  bj-vtoclgft  11321  djucllem  11346  bj-nvel  11434