Theorem elisset 2299

Description: If a class is a member of another class, it is a set. Theorem 6.12 of [Quine] p. 44. (The proof was shortened by Andrew Salmon, 8-Jun-2011.)

Assertion

Ref	Expression
elisset	|- (A e. B -> A e. _V)

Proof of Theorem elisset

Step	Hyp	Ref	Expression
1		exsimpl 1461	. 2 |- (E.x(x = A /\ x e. B) -> E.x x = A)
2		df-clel 1880	. 2 |- (A e. B <-> E.x(x = A /\ x e. B))
3		isset 2296	. 2 |- (A e. _V <-> E.x x = A)
4	1, 2, 3	3imtr4i 236	1 |- (A e. B -> A e. _V)

Syntax hints:   -> wi 3   /\ wa 240   = wceq 1298   e. wcel 1300  E.wex 1326  _Vcvv 2292

This theorem is referenced by:  elisseti 2301  elex 2302  vtoclgf 2345  vtocl2gf 2348  cla4gf 2361  cla4gfOLD 2363  elrabf 2413  sbc5gOLD 2471  sbc6gOLD 2473  sbcieg 2484  elrabsf 2486  elabsg 2488  sbcel1gvOLD 2511  sbcel2gvOLD 2513  hbsbc1gd 2515  hbsbc1gdOLD 2516  hbsbcgd 2517  hbsbcgdOLD 2518  sbccomg 2526  sbcralgOLD 2532  sbcrexgOLD 2534  sbcabel 2535  csbexg 2548  sbcel12gOLD 2553  sbceqdigOLD 2555  csbcomg 2560  csbvarg 2564  hbcsb1g 2567  hbcsbg 2569  hbcsb1gd 2570  hbcsbgd 2571  csbnestg 2581  csbnest1g 2582  sbcnestg 2583  csbidmg 2584  csbabgOLD 2589  eldif 2609  ssv 2636  elun 2741  elin 2786  noel 2879  snidb 3068  ifpr 3077  eluni 3180  eliun 3259  csbopabg 3409  nvel 3450  class2seteq 3472  axpweq 3480  elopab 3559  elon2 3668  ordsssuc2 3758  unexg 3798  difex2OLD 3803  reuuni4 3813  reuhypd 3848  elpwun 3855  ordeleqon 3866  onintrab 3882  sucexg 3891  ordsucelsuc 3902  ordsucelsucOLD 3903  onzsl 3928  onzslOLD 3929  vtoclr 4032  ideqg 4114  ideqgOLD 4115  imasng 4287  elimasni 4292  iniseg 4296  elxp5 4380  funprg 4466  fvelimab 4725  fvelimabOLD 4726  fvopabg 4748  elrnopabg 4773  fopab2 4796  eloprabg 4936  oprabval5 4958  oprabval4g 4960  oprabval4gALT 4961  elrnoprabg 5066  oeordi 5262  mapvalg 5389  pmvalg 5390  elixp2 5408  en3d 5460  fodomr 5547  pwuninel 5550  2pwuninel 5551  iunfi 5659  pwfi 5661  hartog 5693  en2lp 5707  r1ord 5766  r1pw 5797  ondomon 6008  ondomcard 6009  cardinfima 6039  unialeph 6043  cflim 6057  cdaval 6067  elnp 6244  shftf 7764  hashgval 8230  fsum1i 8265  fsum1s 8269  fsum1s2 8270  fsump1s 8273  elcncf 8527  eltopsp 8873  tpsex 8874  istps 8875  eltg 8888  eltg2 8889  iscld 8945  islp 9020  grpidval 9342  isgalem 9449  isring 9465  isvc 9532  vacnlem3 9669  spwval2 9996  grothpw 10134  avril1 10142  dif1card 10177  elghomlem2 10194  elsymgrn 10200  fiv 10212  filmapf 10307  idrval 10374  fora2 10407  isdivrng 10417  hcau 10684  sh 10711  closedsub 10726  ch2 10747  elcnop 11420  ellnop 11421  elunop 11436  elhmop 11437  elcnfn 11446  ellnfn 11447  stel 11786  hstel 11787  bnj1463 13550  epelcNEW 13826  elno 13987  elfix2 14078  elaltxp 14098  elo 14342  moec 14351  snelpwg 14415  pw2eng 14419  infxpg 14422  infsdomnng 14423  sndw2 14429  prnzg 14454  fopab2g 14485  ispr1 14496  cbcpcp 14504  isprj1 14505  iscst1 14519  cur1val 14546  domrancur1b 14548  ubos2 14598  ubos 14599  mxlelt2 14606  mxlelt 14607  mnlelt2 14608  fprod1i 14673  fprod1s 14677  fprod1s2 14678  fprod1s1 14679  fprodp1s 14682  fprodp1s1 14683  fprod1i2 14685  isppm 14715  fnopabco2b 14734  osneisi 14875  distopg 14876  homindlem3 14900  sbtpsines 14905  istopx 14918  efilcp2 14926  cnfilca 14927  clindistop2 14963  istopgrp 14971  trdom 15013  cnvtr 15016  supnufb 15042  supbrr 15048  dualcat2lem 15129  dualded2lem 15130  tarsuc3 15246  valtar 15260  trclval 15271  isseg1 15304  elfiun 15369  hartogOLD 15384  topfneec 15501  islocfin 15506  topmtcl 15525  euuni2 15663  opelopab3 15688  erthdmg 15730  ac6gf 15749  elfzp12 15795  iserzshft2 15829  isumshft2 15830  cla4gft 16406  pltval 16781  pgeval 16794  lubfval 16803  glbfval 16808  glbprople 16812  joinfval 16814  meetfval 16821  p0val 16843  p1val 16844  cmtfval 16937  cvrfval 16987  patoms 17000  grpidvalNEW 17117  grpinvfvalNEW 17125  ringidval 17149  invrfval 17170  plusssfval 17204  ocvfval 17206  csubspset 17208  lineset 17219  pointset 17222  psubspset 17225  pmapfval 17236  paddfval 17258  polfval 17317  psubclset 17346  watomfval 17392  pautset 17395  dilfset 17401  trnfset 17404

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 1305  ax-12 1310  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-ext 1865

This theorem depends on definitions:  df-bi 164  df-an 242  df-ex 1327  df-sb 1536  df-clab 1872  df-cleq 1877  df-clel 1880  df-v 2294

Copyright terms: Public domain