Theorem elex 2610

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 1548	. 2 |- ( E. x ( x = A /\ x e. B ) -> E. x x = A )
2		df-clel 2077	. 2 |- ( A e. B <-> E. x ( x = A /\ x e. B ) )
3		isset 2605	. 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 1284   E.wex 1421   e. wcel 1433   _Vcvv 2601

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 1376  ax-gen 1378  ax-ie1 1422  ax-ie2 1423  ax-8 1435  ax-4 1440  ax-17 1459  ax-i9 1463  ax-ial 1467  ax-ext 2063

This theorem depends on definitions:  df-bi 115  df-sb 1686  df-clab 2068  df-cleq 2074  df-clel 2077  df-v 2603

This theorem is referenced by:  elexi  2611  elexd  2612  elisset  2613  vtoclgft  2649  vtoclgf  2657  vtocl2gf  2660  vtocl3gf  2661  spcimgft  2674  spcimegft  2676  elab4g  2742  elrabf  2747  mob  2774  sbcex  2823  sbcel1v  2876  sbcabel  2895  csbcomg  2929  csbvarg  2933  csbiebt  2942  csbnestgf  2954  csbidmg  2958  sbcco3g  2959  csbco3g  2960  eldif  2982  ssv  3019  elun  3113  elin  3155  snidb  3424  dfopg  3568  eluni  3604  eliun  3682  csbexga  3906  nvel  3910  class2seteq  3937  axpweq  3945  snelpwi  3967  opexg  3983  elopab  4013  epelg  4045  elon2  4131  unexg  4196  reuhypd  4221  sucexg  4242  sucelon  4247  onsucelsucr  4252  sucunielr  4254  en2lp  4297  peano2  4336  peano2b  4355  opelvvg  4407  opeliunxp  4413  opeliunxp2  4494  ideqg  4505  elrnmptg  4604  imasng  4710  iniseg  4717  opswapg  4827  elxp4  4828  elxp5  4829  dmmptg  4838  iota2  4913  fnmpt  5045  fvexg  5214  fvelimab  5250  mptfvex  5277  fvmptdf  5279  fvmptdv2  5281  mpteqb  5282  fvmptt  5283  fvmptf  5284  fvopab6  5285  fsn2  5358  fmptpr  5376  eloprabga  5611  ovmpt2s  5644  ov2gf  5645  ovmpt2dxf  5646  ovmpt2x  5649  ovmpt2ga  5650  ovmpt2df  5652  ovi3  5657  ovelrn  5669  suppssfv  5728  suppssov1  5729  offval3  5781  1stexg  5814  2ndexg  5815  elxp6  5816  elxp7  5817  releldm2  5831  fnmpt2  5848  mpt2fvex  5849  mpt2exg  5854  brtpos2  5889  rdgtfr  5984  rdgruledefgg  5985  frec0g  6006  sucinc2  6049  nntri3or  6095  relelec  6169  ecdmn0m  6171  elinp  6664  addnqprlemfl  6749  addnqprlemfu  6750  mulnqprlemfl  6765  mulnqprlemfu  6766  recexprlemell  6812  recexprlemelu  6813  ibcval5  9690  shftfvalg  9706  clim  10120  climmpt  10139  climshft2  10145  bj-vtoclgft  10585  bj-nvel  10688