Theorem elex 2771

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 1628	. 2 |- ( E. x ( x = A /\ x e. B ) -> E. x x = A )
2		df-clel 2189	. 2 |- ( A e. B <-> E. x ( x = A /\ x e. B ) )
3		isset 2766	. 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 1503   e. wcel 2164   _Vcvv 2760

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 1458  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-ext 2175

This theorem depends on definitions:  df-bi 117  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-v 2762

This theorem is referenced by:  elexi  2772  elexd  2773  elisset  2774  vtoclgft  2810  vtoclgf  2818  vtoclg1f  2819  vtocl2gf  2822  vtocl3gf  2823  spcimgft  2836  spcimegft  2838  elab4g  2909  elrabf  2914  mob  2942  sbcex  2994  sbcel1v  3048  sbcabel  3067  csbcomg  3103  csbvarg  3108  csbiebt  3120  csbnestgf  3133  csbidmg  3137  sbcco3g  3138  csbco3g  3139  eldif  3162  ssv  3201  elun  3300  elin  3342  elpwb  3611  snidb  3648  snssg  3752  dfopg  3802  eluni  3838  eliun  3916  csbexga  4157  nvel  4162  class2seteq  4192  axpweq  4200  snelpwi  4241  opexg  4257  elopab  4288  epelg  4321  elon2  4407  unexg  4474  reuhypd  4502  sucexg  4530  onsucb  4535  onsucelsucr  4540  sucunielr  4542  en2lp  4586  peano2  4627  peano2b  4647  opelvvg  4708  opeliunxp  4714  opeliunxp2  4802  ideqg  4813  elrnmptg  4914  imasng  5030  iniseg  5037  opswapg  5152  elxp4  5153  elxp5  5154  dmmptg  5163  iota2  5244  fnmpt  5380  fvexg  5573  fvelimab  5613  mptfvex  5643  fvmptdf  5645  fvmptdv2  5647  mpteqb  5648  fvmptt  5649  fvmptf  5650  fvopab6  5654  fsn2  5732  fmptpr  5750  eloprabga  6005  ovmpos  6042  ov2gf  6043  ovmpodxf  6044  ovmpox  6047  ovmpoga  6048  ovmpodf  6050  ovi3  6055  ovelrn  6067  suppssfv  6126  suppssov1  6127  offval3  6186  1stexg  6220  2ndexg  6221  elxp6  6222  elxp7  6223  releldm2  6238  fnmpo  6255  mpofvex  6256  mpoexg  6264  opeliunxp2f  6291  brtpos2  6304  rdgtfr  6427  rdgruledefgg  6428  frec0g  6450  sucinc2  6499  nntri3or  6546  relelec  6629  ecdmn0m  6631  mapvalg  6712  pmvalg  6713  elpmg  6718  elixp2  6756  mptelixpg  6788  elixpsn  6789  map1  6866  mapdom1g  6903  mapxpen  6904  fival  7029  elfi2  7031  djulclr  7108  djurclr  7109  djulcl  7110  djurcl  7111  djulclb  7114  inl11  7124  djuss  7129  1stinl  7133  2ndinl  7134  1stinr  7135  2ndinr  7136  ismkvnex  7214  omniwomnimkv  7226  cc4n  7331  elinp  7534  addnqprlemfl  7619  addnqprlemfu  7620  mulnqprlemfl  7635  mulnqprlemfu  7636  recexprlemell  7682  recexprlemelu  7683  wrdexg  10925  wrdsymb0  10946  shftfvalg  10962  clim  11424  climmpt  11443  climshft2  11449  4sqlem2  12527  isstruct2r  12629  slotex  12645  setsvalg  12648  setsfun0  12654  setscom  12658  ressvalsets  12682  ressbasid  12688  restval  12856  topnvalg  12862  tgval  12873  ptex  12875  prdsex  12880  imasex  12888  qusex  12908  qusaddvallemg  12916  xpsfrnel2  12929  plusffvalg  12945  grpidvalg  12956  gsum0g  12979  sgrp1  12994  issubmnd  13023  issubm  13044  grppropstrg  13091  grpinvfvalg  13114  grpinvfng  13116  grpsubfvalg  13117  grpressid  13133  mulgfvalg  13191  mulgex  13193  mulgfng  13194  issubg  13243  subgex  13246  releqgg  13290  eqgex  13291  eqgfval  13292  isghm  13313  ablressid  13405  mgpvalg  13419  mgptopng  13425  rngressid  13450  rngpropd  13451  ringidvalg  13457  dfur2g  13458  issrg  13461  iscrng2  13511  ringressid  13559  opprvalg  13565  reldvdsrsrg  13588  dvdsrex  13594  unitgrp  13612  unitabl  13613  unitlinv  13622  unitrinv  13623  isnzr2  13680  issubrng  13695  issubrg  13717  subrgugrp  13736  aprap  13782  islmod  13787  scaffvalg  13802  lsssetm  13852  islssmg  13854  lspfval  13884  lspval  13886  lspcl  13887  lspex  13891  sraval  13933  rlmvalg  13950  rlmsubg  13954  rlmvnegg  13961  ixpsnbasval  13962  lidlvalg  13967  rspvalg  13968  lidlex  13969  rspex  13970  2idlvalg  13999  zrhvalg  14106  zlmval  14115  toponsspwpwg  14190  eltg  14220  eltg2  14221  restbasg  14336  tgrest  14337  txvalex  14422  txval  14423  ispsmet  14491  ismet  14512  isxmet  14513  xmetunirn  14526  blfvalps  14553  bj-vtoclgft  15267  djucllem  15292  bj-nvel  15389