Theorem elex 2534

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 1481	. 2 |- (E.x(x = A /\ x e. B) -> E.x x = A)
2		df-clel 2009	. 2 |- (A e. B <-> E.x(x = A /\ x e. B))
3		isset 2530	. 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 1223  E.wex 1354   e. wcel 1366   _Vcvv 2526

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 1309  ax-gen 1311  ax-ie1 1355  ax-ie2 1356  ax-8 1368  ax-4 1373  ax-17 1392  ax-i9 1396  ax-ial 1400  ax-ext 1995

This theorem depends on definitions:  df-bi 110  df-sb 1619  df-clab 2000  df-cleq 2006  df-clel 2009  df-v 2528

This theorem is referenced by:  elexi  2535  elisset  2536  vtoclgft  2572  vtoclgf  2580  vtocl2gf  2583  vtocl3gf  2584  spcimgft  2597  spcimegft  2599  elab4g  2659  elrabf  2664  mob  2691  sbcex  2740  sbcabel  2807  csbcomg  2841  csbvarg  2845  csbiebt  2854  csbnestgf  2866  csbidmg  2870  sbcco3g  2871  csbco3g  2872  eldif  2895  ssv  2933  elun  3052  elin  3094  snidb  3365  dfopg  3510  eluni  3546  eliun  3624  csbexga  3848  nvel  3852  class2seteq  3879  axpweq  3887  snelpwi  3911  prelpwi  3913  opexg  3927  elopab  3958  epelg  3990  elon2  4051  unexg  4116  reuhypd  4141  op1stbg  4148  sucexg  4162  sucelon  4167  onsucelsucr  4171  sucunielr  4173  en2lp  4204  peano2  4233  peano2b  4252  opelvvg  4304  opeliunxp  4310  opbrop  4334  opeliunxp2  4391  ideqg  4402  elrnmptg  4501  imasng  4605  iniseg  4612  opswapg  4722  elxp4  4723  elxp5  4724  dmmptg  4733  iota2  4808  fnmpt  4939  fvexg  5107  fvelimab  5142  mptfvex  5169  fvmptdf  5171  fvmptdv2  5173  mpteqb  5174  fvmptt  5175  fvmptf  5176  fvopab6  5177  fsn2  5250  fmptpr  5268  fliftel  5346  eloprabga  5502  ovmpt2s  5535  ov2gf  5536  ovmpt2dxf  5537  ovmpt2x  5540  ovmpt2ga  5541  ovmpt2df  5543  ovi3  5548  ovelrn  5560  suppssfv  5619  suppssov1  5620  offval3  5672  1stexg  5705  2ndexg  5706  elxp6  5707  elxp7  5708  releldm2  5722  fnmpt2  5739  mpt2fvex  5740  mpt2exg  5745  brtpos2  5776  rdgruledefgg  5870  sucinc2  5929  nntri3or  5975  relelec  6045  ecdmn0m  6047  elinp  6314  recexprlemell  6443  recexprlemelu  6444  bj-vtoclgft  8179  bj-nvel  8278