Theorem elisset 1808

Description: If a class is a member of another class, it is a set. Theorem 6.12 of [Quine] p. 44.

Assertion

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

Proof of Theorem elisset

Step	Hyp	Ref	Expression
1		df-clel 1465	. . . 4 |- (A e. B <-> E.x(x = A /\ x e. B))
2		19.40 1090	. . . 4 |- (E.x(x = A /\ x e. B) -> (E.x x = A /\ E.x x e. B))
3	1, 2	sylbi 199	. . 3 |- (A e. B -> (E.x x = A /\ E.x x e. B))
4	3	pm3.26d 321	. 2 |- (A e. B -> E.x x = A)
5		isset 1805	. 2 |- (A e. V <-> E.x x = A)
6	4, 5	sylibr 200	1 |- (A e. B -> A e. V)

Syntax hints:   -> wi 3   /\ wa 223   = wceq 953   e. wcel 955  E.wex 977  Vcvv 1802

This theorem is referenced by:  elisseti 1809  elex 1810  vtoclgf 1837  vtocl2gf 1840  cla4gf 1851  elrabf 1895  sbc5g 1944  sbc6g 1945  sbcieg 1951  elrabsf 1953  elabsg 1955  sbcel1gv 1970  sbcel2gv 1971  hbsbc1gd 1973  hbsbcgd 1974  sbccomg 1979  sbcralg 1984  sbcrexg 1985  sbcabel 1986  csbexg 1998  sbcel12g 2001  sbceqdig 2002  csbcomg 2007  csbvarg 2011  hbcsb1g 2014  hbcsbg 2016  hbcsb1gd 2017  hbcsbgd 2018  csbnestg 2026  csbnest1g 2027  sbcnestg 2028  csbidmg 2029  csbabg 2033  eldif 2047  ssv 2071  elun 2163  elin 2197  noel 2274  ifpr 2417  snidb 2424  eluni 2496  eliun 2560  csbopabg 2668  nvel 2704  class2seteq 2725  elopab 2800  unexg 2865  difex2 2867  reuuni4 2877  reuhyp 2895  elpwun 2901  elon2 2949  ordeleqon 2980  onintrab 3003  sucexg 3039  ordsucelsuc 3063  onzsl 3107  vtoclr 3201  ideqg 3266  imasng 3408  iniseg 3414  elxp5 3440  fvelimab 3750  fvopabg 3770  elrnopabg 3785  fopab2 3808  eloprabg 3992  oprabval5 4014  oprabval4g 4016  elrnoprabg 4108  oeordi 4198  mapvalg 4314  pmvalg 4315  elixp2 4333  en3d 4382  fodomr 4463  en2lp 4574  r1ord 4627  r1pw 4658  ondomon 4828  ondomcard 4829  cardinfima 4863  unialeph 4867  cflim 4881  cdavalt 4891  elnp 5064  shftf 6288  fsum1 6943  fsum1s 6947  fsum1s2 6948  fsump1s 6951  elcncf 7200  eltopsp 7546  tpsex 7547  istps 7548  eltgt 7560  eltg2t 7561  iscld 7611  islp 7685  isring 8078  isvcgOLD 8133  isvc 8138  spwval2 8577  avril1 8723  hcau 8972  sh 8999  closedsub 9014  ch2 9035  elcnopt 9700  ellnopt 9701  elunopt 9716  elhmopt 9717  elcnfnt 9726  ellnfnt 9727  stelt 10051  hstelt 10052  elghomlem2 10288  elsymgrn 10306  elo 10345  moec 10357  fiv 10374  efilcp2 10450  cnfilca 10451  trdom 10479  cnvtr 10482

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 960  ax-12 965  ax-17 968  ax-4 970  ax-5o 972  ax-6o 975  ax-9o 1119  ax-ext 1452

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 978  df-sb 1168  df-clab 1457  df-cleq 1462  df-clel 1465  df-v 1803

Copyright terms: Public domain