Theorem elex 2774

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 1631	. 2 |- ( E. x ( x = A /\ x e. B ) -> E. x x = A )
2		df-clel 2192	. 2 |- ( A e. B <-> E. x ( x = A /\ x e. B ) )
3		isset 2769	. 2 |- ( A e. _V <-> E. x x = A )
4	1, 2, 3	3imtr4i 201	1 |- ( A e. B -> A e. _V )

Syntax hints:   -> wi 4   /\ wa 104   = wceq 1364   E.wex 1506   e. wcel 2167   _Vcvv 2763

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1461  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-v 2765

This theorem is referenced by:  elexi  2775  elexd  2776  elisset  2777  vtoclgft  2814  vtoclgf  2822  vtoclg1f  2823  vtocl2gf  2826  vtocl3gf  2827  spcimgft  2840  spcimegft  2842  elab4g  2913  elrabf  2918  mob  2946  sbcex  2998  sbcel1v  3052  sbcabel  3071  csbcomg  3107  csbvarg  3112  csbiebt  3124  csbnestgf  3137  csbidmg  3141  sbcco3g  3142  csbco3g  3143  eldif  3166  ssv  3206  elun  3305  elin  3347  elpwb  3616  snidb  3653  snssg  3757  dfopg  3807  eluni  3843  eliun  3921  csbexga  4162  nvel  4167  class2seteq  4197  axpweq  4205  snelpwi  4246  opexg  4262  elopab  4293  epelg  4326  elon2  4412  unexg  4479  reuhypd  4507  sucexg  4535  onsucb  4540  onsucelsucr  4545  sucunielr  4547  en2lp  4591  peano2  4632  peano2b  4652  opelvvg  4713  opeliunxp  4719  opeliunxp2  4807  ideqg  4818  elrnmptg  4919  imasng  5035  iniseg  5042  opswapg  5157  elxp4  5158  elxp5  5159  dmmptg  5168  iota2  5249  fnmpt  5385  fvexg  5578  fvelimab  5618  mptfvex  5648  fvmptdf  5650  fvmptdv2  5652  mpteqb  5653  fvmptt  5654  fvmptf  5655  fvopab6  5659  fsn2  5737  fmptpr  5755  eloprabga  6011  ovmpos  6048  ov2gf  6049  ovmpodxf  6050  ovmpox  6053  ovmpoga  6054  ovmpodf  6056  ovi3  6062  ovelrn  6074  suppssfv  6133  suppssov1  6134  offval3  6193  1stexg  6227  2ndexg  6228  elxp6  6229  elxp7  6230  releldm2  6245  fnmpo  6262  mpofvex  6265  mpoexg  6271  opeliunxp2f  6298  brtpos2  6311  rdgtfr  6434  rdgruledefgg  6435  frec0g  6457  sucinc2  6506  nntri3or  6553  relelec  6636  ecdmn0m  6638  mapvalg  6719  pmvalg  6720  elpmg  6725  elixp2  6763  mptelixpg  6795  elixpsn  6796  map1  6873  mapdom1g  6910  mapxpen  6911  fival  7038  elfi2  7040  djulclr  7117  djurclr  7118  djulcl  7119  djurcl  7120  djulclb  7123  inl11  7133  djuss  7138  1stinl  7142  2ndinl  7143  1stinr  7144  2ndinr  7145  ismkvnex  7223  omniwomnimkv  7235  cc4n  7341  elinp  7544  addnqprlemfl  7629  addnqprlemfu  7630  mulnqprlemfl  7645  mulnqprlemfu  7646  recexprlemell  7692  recexprlemelu  7693  wrdexg  10949  wrdsymb0  10970  shftfvalg  10986  clim  11449  climmpt  11468  climshft2  11474  4sqlem2  12569  isstruct2r  12700  slotex  12716  setsvalg  12719  setsfun0  12725  setscom  12729  ressvalsets  12753  ressbasid  12759  restval  12933  topnvalg  12939  tgval  12950  ptex  12952  prdsex  12957  imasex  12974  qusex  12994  qusaddvallemg  13002  xpsfrnel2  13015  plusffvalg  13031  grpidvalg  13042  gsum0g  13065  sgrp1  13080  issubmnd  13109  issubm  13130  grppropstrg  13177  grpinvfvalg  13200  grpinvfng  13202  grpsubfvalg  13203  grpressid  13219  mulgfvalg  13277  mulgex  13279  mulgfng  13280  issubg  13329  subgex  13332  releqgg  13376  eqgex  13377  eqgfval  13378  isghm  13399  ablressid  13491  mgpvalg  13505  mgptopng  13511  rngressid  13536  rngpropd  13537  ringidvalg  13543  dfur2g  13544  issrg  13547  iscrng2  13597  ringressid  13645  opprvalg  13651  reldvdsrsrg  13674  dvdsrex  13680  unitgrp  13698  unitabl  13699  unitlinv  13708  unitrinv  13709  isnzr2  13766  issubrng  13781  issubrg  13803  subrgugrp  13822  aprap  13868  islmod  13873  scaffvalg  13888  lsssetm  13938  islssmg  13940  lspfval  13970  lspval  13972  lspcl  13973  lspex  13977  sraval  14019  rlmvalg  14036  rlmsubg  14040  rlmvnegg  14047  ixpsnbasval  14048  lidlvalg  14053  rspvalg  14054  lidlex  14055  rspex  14056  2idlvalg  14085  zrhvalg  14200  zlmval  14209  toponsspwpwg  14284  eltg  14314  eltg2  14315  restbasg  14430  tgrest  14431  txvalex  14516  txval  14517  ispsmet  14585  ismet  14606  isxmet  14607  xmetunirn  14620  blfvalps  14647  bj-vtoclgft  15447  djucllem  15472  bj-nvel  15569  2omapen  15669