Theorem elisset 1817

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 1472	. . . 4 |- (A e. B <-> E.x(x = A /\ x e. B))
2		19.40 1094	. . . 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 1814	. 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 956   e. wcel 958  E.wex 980  Vcvv 1811

This theorem is referenced by:  elisseti 1818  elex 1819  vtoclgf 1846  vtocl2gf 1849  cla4gf 1860  elrabf 1904  sbc5g 1954  sbc6g 1955  sbcieg 1961  elrabsf 1963  elabsg 1965  sbcel1gv 1980  sbcel2gv 1981  hbsbc1gd 1983  hbsbcgd 1984  sbccomg 1989  sbcralg 1994  sbcrexg 1995  sbcabel 1996  csbexg 2008  sbcel12g 2011  sbceqdig 2012  csbcomg 2017  csbvarg 2021  hbcsb1g 2024  hbcsbg 2026  hbcsb1gd 2027  hbcsbgd 2028  csbnestg 2036  csbnest1g 2037  sbcnestg 2038  csbidmg 2039  csbabg 2043  eldif 2057  ssv 2081  elun 2173  elin 2207  noel 2284  ifpr 2427  snidb 2434  eluni 2506  eliun 2570  csbopabg 2678  nvel 2714  class2seteq 2735  elopab 2811  unexg 2874  difex2 2877  reuuni4 2887  reuhyp 2905  elpwun 2911  elon2 2959  ordeleqon 2990  onintrab 3013  sucexg 3049  ordsucelsuc 3073  onzsl 3117  vtoclr 3211  ideqg 3276  imasng 3424  iniseg 3430  elxp5 3454  fvelimab 3765  fvopabg 3785  elrnopabg 3800  fopab2 3823  eloprabg 4007  oprabval5 4029  oprabval4g 4031  elrnoprabg 4124  oeordi 4214  mapvalg 4330  pmvalg 4331  elixp2 4349  en3d 4401  fodomr 4483  pwuninel 4486  2pwuninel 4487  en2lp 4602  r1ord 4655  r1pw 4686  ondomon 4856  ondomcard 4857  cardinfima 4891  unialeph 4895  cflim 4909  cdavalt 4919  elnp 5092  shftf 6351  fsum1 7005  fsum1s 7009  fsum1s2 7010  fsump1s 7013  elcncf 7265  eltopsp 7604  tpsex 7605  istps 7606  eltgt 7618  eltg2t 7619  iscld 7669  islp 7744  isring 8141  isvc 8200  spwval2 8653  avril1 8784  hcau 9051  sh 9078  closedsub 9093  ch2 9114  elcnopt 9783  ellnopt 9784  elunopt 9799  elhmopt 9800  elcnfnt 9809  ellnfnt 9810  stelt 10141  hstelt 10142  elghomlem2 10383  elsymgrn 10401  elo 10444  moec 10461  fiv 10482  fivOLD 10483  homindlem3 10551  efilcp2 10581  efilcp2OLD 10582  cnfilca 10583  cnfilcaOLD 10584  trdom 10635  cnvtr 10638

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 963  ax-12 968  ax-17 971  ax-4 973  ax-5o 975  ax-6o 978  ax-9o 1123  ax-ext 1459

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 981  df-sb 1172  df-clab 1464  df-cleq 1469  df-clel 1472  df-v 1812

Copyright terms: Public domain