Theorem elisset 1792

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 1449	. . . 4 |- (A e. B <-> E.x(x = A /\ x e. B))
2		19.40 1070	. . . 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 1789	. 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  E.wex 956   = wceq 1099   e. wcel 1105  Vcvv 1786

This theorem is referenced by:  elisseti 1793  elex 1794  vtoclgf 1821  vtocl2gf 1824  cla4gf 1835  elrabf 1876  sbc5g 1925  sbc6g 1926  sbcieg 1932  elrabsf 1934  elabsg 1936  sbcel1gv 1951  sbcel2gv 1952  hbsbc1gd 1954  hbsbcgd 1955  sbccomg 1960  sbcralg 1965  sbcrexg 1966  sbcabel 1967  csbexg 1979  sbcel12g 1982  sbceqdig 1983  csbcomg 1988  csbvarg 1992  hbcsb1g 1995  hbcsbg 1997  hbcsb1gd 1998  hbcsbgd 1999  csbnestg 2007  csbnest1g 2008  sbcnestg 2009  csbidmg 2010  csbabg 2014  eldif 2028  ssv 2052  elun 2144  elin 2178  noel 2255  ifpr 2398  snidb 2405  eluni 2474  eliun 2538  csbopabg 2646  nvel 2682  class2seteq 2703  elopab 2773  unexg 2838  difex2 2840  reuuni4 2850  reuhyp 2868  elpwun 2874  elon2 2922  ordeleqon 2953  onintrab 2976  sucexg 3012  ordsucelsuc 3036  onzsl 3080  vtoclr 3173  opelxp 3176  imasng 3375  iniseg 3381  elxp5 3403  fvelimab 3704  fvopabg 3724  elrnopabg 3739  fopab2 3762  eloprabg 3946  oprabval5 3968  oprabval4g 3970  elrnoprabg 4062  oeordi 4152  mapvalg 4268  pmvalg 4269  elixp2 4287  en3d 4336  fodomr 4417  en2lp 4526  r1ord 4579  r1pw 4610  ondomon 4779  ondomcard 4780  cardinfima 4814  unialeph 4818  cflim 4832  cdavalt 4842  elnp 5015  shftf 6239  fsum1 6894  fsum1s 6898  fsum1s2 6899  fsump1s 6902  elcncf 7151  eltopsp 7497  tpsex 7498  istps 7499  eltgt 7511  eltg2t 7512  iscld 7562  islp 7633  isring 8026  isvcg 8052  elghomlem2 8650  elsymgrn 8668  symggrp 8675  elo 8704  moec 8716  fiv 8731  efilcp2 8800  cnfilca 8801  trdom 8829  cnvtr 8832  avril1 8964  hcau 9201  sh 9229  closedsub 9244  ch2 9265  elcnopt 9914  ellnopt 9915  elunopt 9930  elhmopt 9931  elcnfnt 9940  ellnfnt 9941  stelt 10265  hstelt 10266

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-4 951  ax-5 952  ax-6 953  ax-gen 955  ax-9 1102  ax-12 1104  ax-17 1190  ax-ext 1436

This theorem depends on definitions:  df-bi 147  df-an 225  df-ex 957  df-sb 1155  df-clab 1441  df-cleq 1446  df-clel 1449  df-v 1787

Copyright terms: Public domain