Theorem elex 2763

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 2185	. 2 |- ( A e. B <-> E. x ( x = A /\ x e. B ) )
3		isset 2758	. 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 2160   _Vcvv 2752

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 2171

This theorem depends on definitions:  df-bi 117  df-sb 1774  df-clab 2176  df-cleq 2182  df-clel 2185  df-v 2754

This theorem is referenced by:  elexi  2764  elexd  2765  elisset  2766  vtoclgft  2802  vtoclgf  2810  vtoclg1f  2811  vtocl2gf  2814  vtocl3gf  2815  spcimgft  2828  spcimegft  2830  elab4g  2901  elrabf  2906  mob  2934  sbcex  2986  sbcel1v  3040  sbcabel  3059  csbcomg  3095  csbvarg  3100  csbiebt  3111  csbnestgf  3124  csbidmg  3128  sbcco3g  3129  csbco3g  3130  eldif  3153  ssv  3192  elun  3291  elin  3333  elpwb  3600  snidb  3637  snssg  3741  dfopg  3791  eluni  3827  eliun  3905  csbexga  4146  nvel  4151  class2seteq  4181  axpweq  4189  snelpwi  4230  opexg  4246  elopab  4276  epelg  4308  elon2  4394  unexg  4461  reuhypd  4489  sucexg  4515  onsucb  4520  onsucelsucr  4525  sucunielr  4527  en2lp  4571  peano2  4612  peano2b  4632  opelvvg  4693  opeliunxp  4699  opeliunxp2  4785  ideqg  4796  elrnmptg  4897  imasng  5011  iniseg  5018  opswapg  5133  elxp4  5134  elxp5  5135  dmmptg  5144  iota2  5225  fnmpt  5361  fvexg  5553  fvelimab  5593  mptfvex  5622  fvmptdf  5624  fvmptdv2  5626  mpteqb  5627  fvmptt  5628  fvmptf  5629  fvopab6  5633  fsn2  5711  fmptpr  5729  eloprabga  5983  ovmpos  6020  ov2gf  6021  ovmpodxf  6022  ovmpox  6025  ovmpoga  6026  ovmpodf  6028  ovi3  6033  ovelrn  6045  suppssfv  6102  suppssov1  6103  offval3  6159  1stexg  6192  2ndexg  6193  elxp6  6194  elxp7  6195  releldm2  6210  fnmpo  6227  mpofvex  6228  mpoexg  6236  opeliunxp2f  6263  brtpos2  6276  rdgtfr  6399  rdgruledefgg  6400  frec0g  6422  sucinc2  6471  nntri3or  6518  relelec  6601  ecdmn0m  6603  mapvalg  6684  pmvalg  6685  elpmg  6690  elixp2  6728  mptelixpg  6760  elixpsn  6761  map1  6838  mapdom1g  6875  mapxpen  6876  fival  6999  elfi2  7001  djulclr  7078  djurclr  7079  djulcl  7080  djurcl  7081  djulclb  7084  inl11  7094  djuss  7099  1stinl  7103  2ndinl  7104  1stinr  7105  2ndinr  7106  ismkvnex  7183  omniwomnimkv  7195  cc4n  7300  elinp  7503  addnqprlemfl  7588  addnqprlemfu  7589  mulnqprlemfl  7604  mulnqprlemfu  7605  recexprlemell  7651  recexprlemelu  7652  shftfvalg  10859  clim  11321  climmpt  11340  climshft2  11346  4sqlem2  12421  isstruct2r  12523  slotex  12539  setsvalg  12542  setsfun0  12548  setscom  12552  ressvalsets  12576  ressbasid  12582  restval  12750  topnvalg  12756  tgval  12767  ptex  12769  prdsex  12774  imasex  12782  qusex  12802  qusaddvallemg  12809  xpsfrnel2  12822  plusffvalg  12838  grpidvalg  12849  sgrp1  12874  issubmnd  12903  issubm  12924  grppropstrg  12964  grpinvfvalg  12986  grpinvfng  12988  grpsubfvalg  12989  grpressid  13005  mulgfvalg  13063  mulgex  13065  mulgfng  13066  issubg  13112  subgex  13115  releqgg  13159  eqgex  13160  eqgfval  13161  isghm  13182  ablressid  13272  mgpvalg  13277  mgptopng  13283  rngressid  13308  rngpropd  13309  ringidvalg  13315  dfur2g  13316  issrg  13319  iscrng2  13369  ringressid  13413  opprvalg  13419  reldvdsrsrg  13442  dvdsrex  13448  unitgrp  13466  unitabl  13467  unitlinv  13476  unitrinv  13477  issubrng  13546  issubrg  13568  subrgugrp  13587  aprap  13602  islmod  13607  scaffvalg  13622  lsssetm  13672  islssmg  13674  lspfval  13704  lspval  13706  lspcl  13707  lspex  13711  sraval  13753  rlmvalg  13770  rlmsubg  13774  rlmvnegg  13781  ixpsnbasval  13782  lidlvalg  13787  rspvalg  13788  lidlex  13789  rspex  13790  2idlvalg  13817  zrhvalg  13915  zlmval  13923  toponsspwpwg  13979  eltg  14009  eltg2  14010  restbasg  14125  tgrest  14126  txvalex  14211  txval  14212  ispsmet  14280  ismet  14301  isxmet  14302  xmetunirn  14315  blfvalps  14342  bj-vtoclgft  14985  djucllem  15010  bj-nvel  15107