Theorem elex 2566

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	|- ( 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 1508	. 2 |- ( E. x ( x = A /\ x e. B ) -> E. x x = A )
2		df-clel 2036	. 2 |- ( A e. B <-> E. x ( x = A /\ x e. B ) )
3		isset 2561	. 2 |- ( A e. _V <-> E. x x = A )
4	1, 2, 3	3imtr4i 190	1 |- ( A e. B -> A e. _V )

Syntax hints:   -> wi 4   /\ wa 97   = wceq 1243   E.wex 1381   e. wcel 1393   _Vcvv 2557

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 2559

This theorem is referenced by:  elexi  2567  elisset  2568  vtoclgft  2604  vtoclgf  2612  vtocl2gf  2615  vtocl3gf  2616  spcimgft  2629  spcimegft  2631  elab4g  2691  elrabf  2696  mob  2723  sbcex  2772  sbcabel  2839  csbcomg  2873  csbvarg  2877  csbiebt  2886  csbnestgf  2898  csbidmg  2902  sbcco3g  2903  csbco3g  2904  eldif  2927  ssv  2965  elun  3084  elin  3126  snidb  3401  dfopg  3547  eluni  3583  eliun  3661  csbexga  3885  nvel  3889  class2seteq  3916  axpweq  3924  snelpwi  3948  prelpwi  3950  opexg  3964  elopab  3995  epelg  4027  elon2  4113  unexg  4178  reuhypd  4203  op1stbg  4210  sucexg  4224  sucelon  4229  onsucelsucr  4234  sucunielr  4236  en2lp  4278  peano2  4318  peano2b  4337  opelvvg  4389  opeliunxp  4395  opbrop  4419  opeliunxp2  4476  ideqg  4487  elrnmptg  4586  imasng  4690  iniseg  4697  opswapg  4807  elxp4  4808  elxp5  4809  dmmptg  4818  iota2  4893  fnmpt  5025  fvexg  5194  fvelimab  5229  mptfvex  5256  fvmptdf  5258  fvmptdv2  5260  mpteqb  5261  fvmptt  5262  fvmptf  5263  fvopab6  5264  fsn2  5337  fmptpr  5355  fliftel  5433  eloprabga  5591  ovmpt2s  5624  ov2gf  5625  ovmpt2dxf  5626  ovmpt2x  5629  ovmpt2ga  5630  ovmpt2df  5632  ovi3  5637  ovelrn  5649  suppssfv  5708  suppssov1  5709  offval3  5761  1stexg  5794  2ndexg  5795  elxp6  5796  elxp7  5797  releldm2  5811  fnmpt2  5828  mpt2fvex  5829  mpt2exg  5834  brtpos2  5866  rdgtfr  5961  rdgruledefgg  5962  frec0g  5983  sucinc2  6026  nntri3or  6072  relelec  6146  ecdmn0m  6148  elinp  6570  addnqprlemfl  6655  addnqprlemfu  6656  mulnqprlemfl  6671  mulnqprlemfu  6672  recexprlemell  6718  recexprlemelu  6719  shftfvalg  9393  clim  9776  climmpt  9795  climshft2  9801  bj-vtoclgft  9888  bj-nvel  9991