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  3205  elun  3304  elin  3346  elpwb  3615  snidb  3652  snssg  3756  dfopg  3806  eluni  3842  eliun  3920  csbexga  4161  nvel  4166  class2seteq  4196  axpweq  4204  snelpwi  4245  opexg  4261  elopab  4292  epelg  4325  elon2  4411  unexg  4478  reuhypd  4506  sucexg  4534  onsucb  4539  onsucelsucr  4544  sucunielr  4546  en2lp  4590  peano2  4631  peano2b  4651  opelvvg  4712  opeliunxp  4718  opeliunxp2  4806  ideqg  4817  elrnmptg  4918  imasng  5034  iniseg  5041  opswapg  5156  elxp4  5157  elxp5  5158  dmmptg  5167  iota2  5248  fnmpt  5384  fvexg  5577  fvelimab  5617  mptfvex  5647  fvmptdf  5649  fvmptdv2  5651  mpteqb  5652  fvmptt  5653  fvmptf  5654  fvopab6  5658  fsn2  5736  fmptpr  5754  eloprabga  6009  ovmpos  6046  ov2gf  6047  ovmpodxf  6048  ovmpox  6051  ovmpoga  6052  ovmpodf  6054  ovi3  6060  ovelrn  6072  suppssfv  6131  suppssov1  6132  offval3  6191  1stexg  6225  2ndexg  6226  elxp6  6227  elxp7  6228  releldm2  6243  fnmpo  6260  mpofvex  6263  mpoexg  6269  opeliunxp2f  6296  brtpos2  6309  rdgtfr  6432  rdgruledefgg  6433  frec0g  6455  sucinc2  6504  nntri3or  6551  relelec  6634  ecdmn0m  6636  mapvalg  6717  pmvalg  6718  elpmg  6723  elixp2  6761  mptelixpg  6793  elixpsn  6794  map1  6871  mapdom1g  6908  mapxpen  6909  fival  7036  elfi2  7038  djulclr  7115  djurclr  7116  djulcl  7117  djurcl  7118  djulclb  7121  inl11  7131  djuss  7136  1stinl  7140  2ndinl  7141  1stinr  7142  2ndinr  7143  ismkvnex  7221  omniwomnimkv  7233  cc4n  7338  elinp  7541  addnqprlemfl  7626  addnqprlemfu  7627  mulnqprlemfl  7642  mulnqprlemfu  7643  recexprlemell  7689  recexprlemelu  7690  wrdexg  10946  wrdsymb0  10967  shftfvalg  10983  clim  11446  climmpt  11465  climshft2  11471  4sqlem2  12558  isstruct2r  12689  slotex  12705  setsvalg  12708  setsfun0  12714  setscom  12718  ressvalsets  12742  ressbasid  12748  restval  12916  topnvalg  12922  tgval  12933  ptex  12935  prdsex  12940  imasex  12948  qusex  12968  qusaddvallemg  12976  xpsfrnel2  12989  plusffvalg  13005  grpidvalg  13016  gsum0g  13039  sgrp1  13054  issubmnd  13083  issubm  13104  grppropstrg  13151  grpinvfvalg  13174  grpinvfng  13176  grpsubfvalg  13177  grpressid  13193  mulgfvalg  13251  mulgex  13253  mulgfng  13254  issubg  13303  subgex  13306  releqgg  13350  eqgex  13351  eqgfval  13352  isghm  13373  ablressid  13465  mgpvalg  13479  mgptopng  13485  rngressid  13510  rngpropd  13511  ringidvalg  13517  dfur2g  13518  issrg  13521  iscrng2  13571  ringressid  13619  opprvalg  13625  reldvdsrsrg  13648  dvdsrex  13654  unitgrp  13672  unitabl  13673  unitlinv  13682  unitrinv  13683  isnzr2  13740  issubrng  13755  issubrg  13777  subrgugrp  13796  aprap  13842  islmod  13847  scaffvalg  13862  lsssetm  13912  islssmg  13914  lspfval  13944  lspval  13946  lspcl  13947  lspex  13951  sraval  13993  rlmvalg  14010  rlmsubg  14014  rlmvnegg  14021  ixpsnbasval  14022  lidlvalg  14027  rspvalg  14028  lidlex  14029  rspex  14030  2idlvalg  14059  zrhvalg  14174  zlmval  14183  toponsspwpwg  14258  eltg  14288  eltg2  14289  restbasg  14404  tgrest  14405  txvalex  14490  txval  14491  ispsmet  14559  ismet  14580  isxmet  14581  xmetunirn  14594  blfvalps  14621  bj-vtoclgft  15421  djucllem  15446  bj-nvel  15543