Theorem elisset 1813

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 1470	. . . 4 |- (A e. B <-> E.x(x = A /\ x e. B))
2		19.40 1092	. . . 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 1810	. 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 954   e. wcel 956  E.wex 978  Vcvv 1807

This theorem is referenced by:  elisseti 1814  elex 1815  vtoclgf 1842  vtocl2gf 1845  cla4gf 1856  elrabf 1900  sbc5g 1950  sbc6g 1951  sbcieg 1957  elrabsf 1959  elabsg 1961  sbcel1gv 1976  sbcel2gv 1977  hbsbc1gd 1979  hbsbcgd 1980  sbccomg 1985  sbcralg 1990  sbcrexg 1991  sbcabel 1992  csbexg 2004  sbcel12g 2007  sbceqdig 2008  csbcomg 2013  csbvarg 2017  hbcsb1g 2020  hbcsbg 2022  hbcsb1gd 2023  hbcsbgd 2024  csbnestg 2032  csbnest1g 2033  sbcnestg 2034  csbidmg 2035  csbabg 2039  eldif 2053  ssv 2077  elun 2169  elin 2203  noel 2280  ifpr 2423  snidb 2430  eluni 2501  eliun 2565  csbopabg 2673  nvel 2709  class2seteq 2730  elopab 2806  unexg 2869  difex2 2872  reuuni4 2882  reuhyp 2900  elpwun 2906  elon2 2954  ordeleqon 2985  onintrab 3008  sucexg 3044  ordsucelsuc 3068  onzsl 3112  vtoclr 3206  ideqg 3271  imasng 3416  iniseg 3422  elxp5 3446  fvelimab 3756  fvopabg 3776  elrnopabg 3791  fopab2 3814  eloprabg 3998  oprabval5 4020  oprabval4g 4022  elrnoprabg 4114  oeordi 4204  mapvalg 4320  pmvalg 4321  elixp2 4339  en3d 4388  fodomr 4469  pwuninel 4472  2pwuninel 4473  en2lp 4582  r1ord 4635  r1pw 4666  ondomon 4836  ondomcard 4837  cardinfima 4871  unialeph 4875  cflim 4889  cdavalt 4899  elnp 5072  shftf 6296  fsum1 6951  fsum1s 6955  fsum1s2 6956  fsump1s 6959  elcncf 7208  eltopsp 7554  tpsex 7555  istps 7556  eltgt 7568  eltg2t 7569  iscld 7619  islp 7694  isring 8093  isvc 8152  spwval2 8595  avril1 8723  hcau 8990  sh 9017  closedsub 9032  ch2 9053  elcnopt 9723  ellnopt 9724  elunopt 9739  elhmopt 9740  elcnfnt 9749  ellnfnt 9750  stelt 10079  hstelt 10080  elghomlem2 10317  elsymgrn 10335  elo 10381  moec 10393  fiv 10410  efilcp2 10486  cnfilca 10487  trdom 10515  cnvtr 10518

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 961  ax-12 966  ax-17 969  ax-4 971  ax-5o 973  ax-6o 976  ax-9o 1121  ax-ext 1457

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 979  df-sb 1170  df-clab 1462  df-cleq 1467  df-clel 1470  df-v 1808

Copyright terms: Public domain