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  5387  fvexg  5580  fvelimab  5620  mptfvex  5650  fvmptdf  5652  fvmptdv2  5654  mpteqb  5655  fvmptt  5656  fvmptf  5657  fvopab6  5661  fsn2  5739  fmptpr  5757  eloprabga  6013  ovmpos  6050  ov2gf  6051  ovmpodxf  6052  ovmpox  6055  ovmpoga  6056  ovmpodf  6058  ovi3  6064  ovelrn  6076  suppssfv  6135  suppssov1  6136  offval3  6200  1stexg  6234  2ndexg  6235  elxp6  6236  elxp7  6237  releldm2  6252  fnmpo  6269  mpofvex  6272  mpoexg  6278  opeliunxp2f  6305  brtpos2  6318  rdgtfr  6441  rdgruledefgg  6442  frec0g  6464  sucinc2  6513  nntri3or  6560  relelec  6643  ecdmn0m  6645  mapvalg  6726  pmvalg  6727  elpmg  6732  elixp2  6770  mptelixpg  6802  elixpsn  6803  map1  6880  mapdom1g  6917  mapxpen  6918  fival  7045  elfi2  7047  djulclr  7124  djurclr  7125  djulcl  7126  djurcl  7127  djulclb  7130  inl11  7140  djuss  7145  1stinl  7149  2ndinl  7150  1stinr  7151  2ndinr  7152  ismkvnex  7230  omniwomnimkv  7242  isacnm  7286  cc4n  7354  elinp  7558  addnqprlemfl  7643  addnqprlemfu  7644  mulnqprlemfl  7659  mulnqprlemfu  7660  recexprlemell  7706  recexprlemelu  7707  wrdexg  10963  wrdsymb0  10984  shftfvalg  11000  clim  11463  climmpt  11482  climshft2  11488  4sqlem2  12583  isstruct2r  12714  slotex  12730  setsvalg  12733  setsfun0  12739  setscom  12743  ressvalsets  12767  ressbasid  12773  restval  12947  topnvalg  12953  tgval  12964  ptex  12966  prdsex  12971  pwsval  12993  pwsbas  12994  pwselbasb  12995  pwssnf1o  13000  imasex  13007  qusex  13027  qusaddvallemg  13035  xpsfrnel2  13048  plusffvalg  13064  grpidvalg  13075  gsum0g  13098  sgrp1  13113  issubmnd  13144  pws0g  13153  issubm  13174  grppropstrg  13221  grpinvfvalg  13244  grpinvfng  13246  grpsubfvalg  13247  grpressid  13263  mulgfvalg  13327  mulgex  13329  mulgfng  13330  issubg  13379  subgex  13382  releqgg  13426  eqgex  13427  eqgfval  13428  isghm  13449  ablressid  13541  mgpvalg  13555  mgptopng  13561  rngressid  13586  rngpropd  13587  ringidvalg  13593  dfur2g  13594  issrg  13597  iscrng2  13647  ringressid  13695  opprvalg  13701  reldvdsrsrg  13724  dvdsrex  13730  unitgrp  13748  unitabl  13749  unitlinv  13758  unitrinv  13759  isnzr2  13816  issubrng  13831  issubrg  13853  subrgugrp  13872  aprap  13918  islmod  13923  scaffvalg  13938  lsssetm  13988  islssmg  13990  lspfval  14020  lspval  14022  lspcl  14023  lspex  14027  sraval  14069  rlmvalg  14086  rlmsubg  14090  rlmvnegg  14097  ixpsnbasval  14098  lidlvalg  14103  rspvalg  14104  lidlex  14105  rspex  14106  2idlvalg  14135  zrhvalg  14250  zlmval  14259  toponsspwpwg  14342  eltg  14372  eltg2  14373  restbasg  14488  tgrest  14489  txvalex  14574  txval  14575  ispsmet  14643  ismet  14664  isxmet  14665  xmetunirn  14678  blfvalps  14705  bj-vtoclgft  15505  djucllem  15530  bj-nvel  15627  2omapen  15727