Theorem elex 2783

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 1640	. 2 |- ( E. x ( x = A /\ x e. B ) -> E. x x = A )
2		df-clel 2201	. 2 |- ( A e. B <-> E. x ( x = A /\ x e. B ) )
3		isset 2778	. 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 1373   E.wex 1515   e. wcel 2176   _Vcvv 2772

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 1470  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-ext 2187

This theorem depends on definitions:  df-bi 117  df-sb 1786  df-clab 2192  df-cleq 2198  df-clel 2201  df-v 2774

This theorem is referenced by:  elexi  2784  elexd  2785  elisset  2786  vtoclgft  2823  vtoclgf  2831  vtoclg1f  2832  vtocl2gf  2835  vtocl3gf  2836  spcimgft  2849  spcimegft  2851  elab4g  2922  elrabf  2927  mob  2955  sbcex  3007  sbcel1v  3061  sbcabel  3080  csbcomg  3116  csbvarg  3121  csbiebt  3133  csbnestgf  3146  csbidmg  3150  sbcco3g  3151  csbco3g  3152  eldif  3175  ssv  3215  elun  3314  elin  3356  elpwb  3626  snidb  3663  snssg  3767  dfopg  3817  eluni  3853  eliun  3931  csbexga  4173  nvel  4178  class2seteq  4208  axpweq  4216  snelpwi  4257  opexg  4273  elopab  4305  epelg  4338  elon2  4424  unexg  4491  reuhypd  4519  sucexg  4547  onsucb  4552  onsucelsucr  4557  sucunielr  4559  en2lp  4603  peano2  4644  peano2b  4664  opelvvg  4725  opeliunxp  4731  opeliunxp2  4819  ideqg  4830  elrnmptg  4931  imasng  5048  iniseg  5055  opswapg  5170  elxp4  5171  elxp5  5172  dmmptg  5181  iota2  5262  fnmpt  5404  fvexg  5597  fvelimab  5637  mptfvex  5667  fvmptdf  5669  fvmptdv2  5671  mpteqb  5672  fvmptt  5673  fvmptf  5674  fvopab6  5678  fsn2  5756  fmptpr  5778  eloprabga  6034  ovmpos  6071  ov2gf  6072  ovmpodxf  6073  ovmpox  6076  ovmpoga  6077  ovmpodf  6079  ovi3  6085  ovelrn  6097  suppssfv  6156  suppssov1  6157  offval3  6221  1stexg  6255  2ndexg  6256  elxp6  6257  elxp7  6258  releldm2  6273  fnmpo  6290  mpofvex  6293  mpoexg  6299  opeliunxp2f  6326  brtpos2  6339  rdgtfr  6462  rdgruledefgg  6463  frec0g  6485  sucinc2  6534  nntri3or  6581  relelec  6664  ecdmn0m  6666  mapvalg  6747  pmvalg  6748  elpmg  6753  elixp2  6791  mptelixpg  6823  elixpsn  6824  map1  6906  rex2dom  6912  mapdom1g  6946  mapxpen  6947  fival  7074  elfi2  7076  djulclr  7153  djurclr  7154  djulcl  7155  djurcl  7156  djulclb  7159  inl11  7169  djuss  7174  1stinl  7178  2ndinl  7179  1stinr  7180  2ndinr  7181  ismkvnex  7259  omniwomnimkv  7271  isacnm  7317  cc4n  7385  elinp  7589  addnqprlemfl  7674  addnqprlemfu  7675  mulnqprlemfl  7690  mulnqprlemfu  7691  recexprlemell  7737  recexprlemelu  7738  wrdexg  11007  wrdsymb0  11028  lswwrd  11042  ccatfvalfi  11051  swrdval  11104  swrd00g  11105  pfxval  11130  shftfvalg  11162  clim  11625  climmpt  11644  climshft2  11650  4sqlem2  12745  isstruct2r  12876  slotex  12892  setsvalg  12895  setsfun0  12901  setscom  12905  ressvalsets  12929  ressbasid  12935  restval  13110  topnvalg  13116  tgval  13127  ptex  13129  prdsex  13134  pwsval  13156  pwsbas  13157  pwselbasb  13158  pwssnf1o  13163  imasex  13170  qusex  13190  qusaddvallemg  13198  xpsfrnel2  13211  plusffvalg  13227  grpidvalg  13238  gsum0g  13261  sgrp1  13276  issubmnd  13307  pws0g  13316  issubm  13337  grppropstrg  13384  grpinvfvalg  13407  grpinvfng  13409  grpsubfvalg  13410  grpressid  13426  mulgfvalg  13490  mulgex  13492  mulgfng  13493  issubg  13542  subgex  13545  releqgg  13589  eqgex  13590  eqgfval  13591  isghm  13612  ablressid  13704  mgpvalg  13718  mgptopng  13724  rngressid  13749  rngpropd  13750  ringidvalg  13756  dfur2g  13757  issrg  13760  iscrng2  13810  ringressid  13858  opprvalg  13864  reldvdsrsrg  13887  dvdsrex  13893  unitgrp  13911  unitabl  13912  unitlinv  13921  unitrinv  13922  isnzr2  13979  issubrng  13994  issubrg  14016  subrgugrp  14035  aprap  14081  islmod  14086  scaffvalg  14101  lsssetm  14151  islssmg  14153  lspfval  14183  lspval  14185  lspcl  14186  lspex  14190  sraval  14232  rlmvalg  14249  rlmsubg  14253  rlmvnegg  14260  ixpsnbasval  14261  lidlvalg  14266  rspvalg  14267  lidlex  14268  rspex  14269  2idlvalg  14298  zrhvalg  14413  zlmval  14422  mplvalcoe  14485  mplbascoe  14486  mplplusgg  14498  toponsspwpwg  14527  eltg  14557  eltg2  14558  restbasg  14673  tgrest  14674  txvalex  14759  txval  14760  ispsmet  14828  ismet  14849  isxmet  14850  xmetunirn  14863  blfvalps  14890  vtxvalg  15648  iedgvalg  15649  edgvalg  15687  bj-vtoclgft  15748  djucllem  15773  bj-nvel  15870  2omapen  15970