Theorem elex 2814

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 1665	. 2 |- ( E. x ( x = A /\ x e. B ) -> E. x x = A )
2		df-clel 2227	. 2 |- ( A e. B <-> E. x ( x = A /\ x e. B ) )
3		isset 2809	. 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 1397   E.wex 1540   e. wcel 2202   _Vcvv 2802

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 1495  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-v 2804

This theorem is referenced by:  elexi  2815  elexd  2816  elisset  2817  vtoclgft  2854  vtoclgf  2862  vtoclg1f  2863  vtocl2gf  2866  vtocl3gf  2867  spcimgft  2882  spcimegft  2884  elab4g  2955  elrabf  2960  mob  2988  sbcex  3040  sbcel1v  3094  sbcabel  3114  csbcomg  3150  csbvarg  3155  csbiebt  3167  csbnestgf  3180  csbidmg  3184  sbcco3g  3185  csbco3g  3186  eldif  3209  ssv  3249  elun  3348  elin  3390  elif  3617  elpwb  3662  snidb  3699  snssg  3807  dfopg  3860  eluni  3896  eliun  3974  csbexga  4217  nvel  4222  class2seteq  4253  axpweq  4261  snelpwi  4303  opexg  4320  elopab  4352  epelg  4387  elon2  4473  unexg  4540  reuhypd  4568  sucexg  4596  onsucb  4601  onsucelsucr  4606  sucunielr  4608  en2lp  4652  peano2  4693  peano2b  4713  opelvvg  4775  opeliunxp  4781  opeliunxp2  4870  ideqg  4881  elrnmptg  4984  imasng  5101  iniseg  5108  opswapg  5223  elxp4  5224  elxp5  5225  dmmptg  5234  iota2  5316  fnmpt  5459  fvexg  5658  fvelimab  5702  mptfvex  5732  fvmptdf  5734  fvmptdv2  5736  mpteqb  5737  fvmptt  5738  fvmptf  5739  fvopab6  5743  fsn2  5821  fmptpr  5846  eloprabga  6108  ovmpos  6145  ov2gf  6146  ovmpodxf  6147  ovmpox  6150  ovmpoga  6151  ovmpodf  6153  ovi3  6159  ovelrn  6171  suppssfv  6231  suppssov1  6232  offval3  6296  1stexg  6330  2ndexg  6331  elxp6  6332  elxp7  6333  releldm2  6348  fnmpo  6367  mpofvex  6370  mpoexg  6376  opeliunxp2f  6404  brtpos2  6417  rdgtfr  6540  rdgruledefgg  6541  frec0g  6563  sucinc2  6614  nntri3or  6661  relelec  6744  ecdmn0m  6746  mapvalg  6827  pmvalg  6828  elpmg  6833  elixp2  6871  mptelixpg  6903  elixpsn  6904  map1  6987  rex2dom  6996  mapdom1g  7033  mapxpen  7034  fival  7169  elfi2  7171  djulclr  7248  djurclr  7249  djulcl  7250  djurcl  7251  djulclb  7254  inl11  7264  djuss  7269  1stinl  7273  2ndinl  7274  1stinr  7275  2ndinr  7276  ismkvnex  7354  omniwomnimkv  7366  isacnm  7418  cc4n  7490  elinp  7694  addnqprlemfl  7779  addnqprlemfu  7780  mulnqprlemfl  7795  mulnqprlemfu  7796  recexprlemell  7842  recexprlemelu  7843  wrdexg  11128  wrdsymb0  11150  lswwrd  11164  ccatfvalfi  11173  swrdval  11233  swrd00g  11234  pfxval  11259  cats1fvn  11349  cats1fvnd  11350  s2fv1g  11373  s2leng  11374  s2dmg  11375  shftfvalg  11396  clim  11859  climmpt  11878  climshft2  11884  4sqlem2  12980  isstruct2r  13111  slotex  13127  setsvalg  13130  setsfun0  13136  setscom  13140  ressvalsets  13165  ressbasid  13171  restval  13346  topnvalg  13352  tgval  13363  ptex  13365  prdsex  13370  pwsval  13392  pwsbas  13393  pwselbasb  13394  pwssnf1o  13399  imasex  13406  qusex  13426  qusaddvallemg  13434  xpsfrnel2  13447  plusffvalg  13463  grpidvalg  13474  gsum0g  13497  sgrp1  13512  issubmnd  13543  pws0g  13552  issubm  13573  grppropstrg  13620  grpinvfvalg  13643  grpinvfng  13645  grpsubfvalg  13646  grpressid  13662  mulgfvalg  13726  mulgex  13728  mulgfng  13729  issubg  13778  subgex  13781  releqgg  13825  eqgex  13826  eqgfval  13827  isghm  13848  ablressid  13940  mgpvalg  13955  mgptopng  13961  rngressid  13986  rngpropd  13987  ringidvalg  13993  dfur2g  13994  issrg  13997  iscrng2  14047  ringressid  14095  opprvalg  14101  dvdsrex  14131  unitgrp  14149  unitabl  14150  unitlinv  14159  unitrinv  14160  isnzr2  14217  issubrng  14232  issubrg  14254  subrgugrp  14273  aprap  14319  islmod  14324  scaffvalg  14339  lsssetm  14389  islssmg  14391  lspfval  14421  lspval  14423  lspcl  14424  lspex  14428  sraval  14470  rlmvalg  14487  rlmsubg  14491  rlmvnegg  14498  ixpsnbasval  14499  lidlvalg  14504  rspvalg  14505  lidlex  14506  rspex  14507  2idlvalg  14536  zrhvalg  14651  zlmval  14660  mplvalcoe  14723  mplbascoe  14724  mplplusgg  14736  toponsspwpwg  14765  eltg  14795  eltg2  14796  restbasg  14911  tgrest  14912  txvalex  14997  txval  14998  ispsmet  15066  ismet  15087  isxmet  15088  xmetunirn  15101  blfvalps  15128  vtxvalg  15886  iedgvalg  15887  vtxex  15888  edgvalg  15929  vtxdgfval  16158  wksfval  16192  iswlkg  16199  wlkvtxeledgg  16214  trlsfvalg  16253  clwwlkg  16263  clwwlkng  16275  eupthsg  16315  bj-vtoclgft  16422  djucllem  16447  bj-nvel  16543  2omapen  16646  pw1mapen  16648