Theorem elisset 1354

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 1099	. . . 4 |- (A e. B <-> E.x(x = A /\ x e. B))
2		19.40 773	. . . 4 |- (E.x(x = A /\ x e. B) -> (E.x x = A /\ E.x x e. B))
3	1, 2	sylbi 174	. . 3 |- (A e. B -> (E.x x = A /\ E.x x e. B))
4	3	pm3.26d 258	. 2 |- (A e. B -> E.x x = A)
5		isset 1351	. 2 |- (A e. V <-> E.x x = A)
6	4, 5	sylibr 175	1 |- (A e. B -> A e. V)

Syntax hints:   -> wi 2   /\ wa 196  E.wex 678   = wceq 1091   e. wcel 1092  Vcvv 1348

This theorem is referenced by:  elisseti 1355  elex 1356  vtoclgf 1382  vtocl2gf 1385  cla4gf 1394  elrabf 1421  sbc5g 1450  sbc6g 1451  elrabsf 1456  sbcel1 1466  sbcel2 1467  eldif 1496  ssv 1520  reuhyp 1581  elun 1601  elin 1635  noel 1711  snidb 1829  eluni 1922  difex2 1951  reuuni4 1959  eliun 1998  elopab 2110  elon2 2210  ordeleqon 2241  onintrab 2268  sucexg 2302  ordsucelsuc 2324  onzsl 2367  vtoclr 2449  opelxp 2452  iniseg 2619  elxp5 2641  fvopabg 2872  fvelrn 2883  fopab2 2891  oprabval4g 3053  mapvalg 3263  en3d 3304  en2lp 3453  r1ord 3499  r1pw 3529  ondomon 3662  ondomcard 3663  cardinfima 3696  cflim 3704  cdavalt 3716  elnp 3886  hcauchy 5103  sh 5116  closedsub 5128  ch2 5149  stelt 5671

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-gen 677  ax-9 799  ax-12 802  ax-17 925  ax-ext 1074

This theorem depends on definitions:  df-bi 128  df-an 198  df-ex 679  df-sb 853  df-clab 1093  df-cleq 1097  df-clel 1099  df-v 1349

metamath.org