Theorem elex 2749

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 1617	. 2 |- ( E. x ( x = A /\ x e. B ) -> E. x x = A )
2		df-clel 2173	. 2 |- ( A e. B <-> E. x ( x = A /\ x e. B ) )
3		isset 2744	. 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 1353   E.wex 1492   e. wcel 2148   _Vcvv 2738

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 1447  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-v 2740

This theorem is referenced by:  elexi  2750  elexd  2751  elisset  2752  vtoclgft  2788  vtoclgf  2796  vtoclg1f  2797  vtocl2gf  2800  vtocl3gf  2801  spcimgft  2814  spcimegft  2816  elab4g  2887  elrabf  2892  mob  2920  sbcex  2972  sbcel1v  3026  sbcabel  3045  csbcomg  3081  csbvarg  3086  csbiebt  3097  csbnestgf  3110  csbidmg  3114  sbcco3g  3115  csbco3g  3116  eldif  3139  ssv  3178  elun  3277  elin  3319  elpwb  3586  snidb  3623  snssg  3727  dfopg  3777  eluni  3813  eliun  3891  csbexga  4132  nvel  4137  class2seteq  4164  axpweq  4172  snelpwi  4213  opexg  4229  elopab  4259  epelg  4291  elon2  4377  unexg  4444  reuhypd  4472  sucexg  4498  onsucb  4503  onsucelsucr  4508  sucunielr  4510  en2lp  4554  peano2  4595  peano2b  4615  opelvvg  4676  opeliunxp  4682  opeliunxp2  4768  ideqg  4779  elrnmptg  4880  imasng  4994  iniseg  5001  opswapg  5116  elxp4  5117  elxp5  5118  dmmptg  5127  iota2  5207  fnmpt  5343  fvexg  5535  fvelimab  5573  mptfvex  5602  fvmptdf  5604  fvmptdv2  5606  mpteqb  5607  fvmptt  5608  fvmptf  5609  fvopab6  5613  fsn2  5691  fmptpr  5709  eloprabga  5962  ovmpos  5998  ov2gf  5999  ovmpodxf  6000  ovmpox  6003  ovmpoga  6004  ovmpodf  6006  ovi3  6011  ovelrn  6023  suppssfv  6079  suppssov1  6080  offval3  6135  1stexg  6168  2ndexg  6169  elxp6  6170  elxp7  6171  releldm2  6186  fnmpo  6203  mpofvex  6204  mpoexg  6212  opeliunxp2f  6239  brtpos2  6252  rdgtfr  6375  rdgruledefgg  6376  frec0g  6398  sucinc2  6447  nntri3or  6494  relelec  6575  ecdmn0m  6577  mapvalg  6658  pmvalg  6659  elpmg  6664  elixp2  6702  mptelixpg  6734  elixpsn  6735  map1  6812  mapdom1g  6847  mapxpen  6848  fival  6969  elfi2  6971  djulclr  7048  djurclr  7049  djulcl  7050  djurcl  7051  djulclb  7054  inl11  7064  djuss  7069  1stinl  7073  2ndinl  7074  1stinr  7075  2ndinr  7076  ismkvnex  7153  omniwomnimkv  7165  cc4n  7270  elinp  7473  addnqprlemfl  7558  addnqprlemfu  7559  mulnqprlemfl  7574  mulnqprlemfu  7575  recexprlemell  7621  recexprlemelu  7622  shftfvalg  10827  clim  11289  climmpt  11308  climshft2  11314  4sqlem2  12387  isstruct2r  12473  slotex  12489  setsvalg  12492  setsfun0  12498  setscom  12502  ressvalsets  12524  restval  12694  topnvalg  12700  tgval  12711  ptex  12713  prdsex  12718  imasex  12726  qusaddvallemg  12752  xpsfrnel2  12765  plusffvalg  12781  grpidvalg  12792  sgrp1  12816  issubmnd  12843  issubm  12863  grppropstrg  12895  grpinvfvalg  12915  grpinvfng  12917  grpsubfvalg  12918  grpressid  12931  mulgfvalg  12985  mulgfng  12987  issubg  13033  subgex  13036  releqgg  13080  eqgfval  13081  mgpvalg  13133  mgptopng  13139  ringidvalg  13144  dfur2g  13145  issrg  13148  iscrng2  13198  ringressid  13238  opprvalg  13241  reldvdsrsrg  13261  dvdsrex  13267  unitgrp  13285  unitabl  13286  unitlinv  13295  unitrinv  13296  issubrg  13342  subrgugrp  13361  aprap  13376  islmod  13381  scaffvalg  13396  toponsspwpwg  13525  eltg  13555  eltg2  13556  restbasg  13671  tgrest  13672  txvalex  13757  txval  13758  ispsmet  13826  ismet  13847  isxmet  13848  xmetunirn  13861  blfvalps  13888  bj-vtoclgft  14530  djucllem  14555  bj-nvel  14652