Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  nalset Unicode version

Theorem nalset 4048
 Description: No set contains all sets. Theorem 41 of [Suppes] p. 30. (Contributed by NM, 23-Aug-1993.)
Assertion
Ref Expression
nalset
Distinct variable group:   ,

Proof of Theorem nalset
StepHypRef Expression
1 alexn 1577 . 2
2 ax-sep 4038 . . 3
3 elequ1 1831 . . . . . . 7
4 elequ1 1831 . . . . . . . 8
5 elequ1 1831 . . . . . . . . . 10
6 elequ2 1832 . . . . . . . . . 10
75, 6bitrd 246 . . . . . . . . 9
87notbid 287 . . . . . . . 8
94, 8anbi12d 694 . . . . . . 7
103, 9bibi12d 314 . . . . . 6
1110a4v 1996 . . . . 5
12 pclem6 901 . . . . 5
1311, 12syl 17 . . . 4
1413eximi 1574 . . 3
152, 14ax-mp 10 . 2
161, 15mpgbi 1543 1
 Colors of variables: wff set class Syntax hints:   wn 5   wb 178   wa 360  wal 1532  wex 1537   wceq 1619   wcel 1621 This theorem is referenced by:  vprc  4049  kmlem2  7661 This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-gen 1536  ax-8 1623  ax-13 1625  ax-14 1626  ax-17 1628  ax-9 1684  ax-4 1692  ax-sep 4038 This theorem depends on definitions:  df-bi 179  df-an 362  df-tru 1315  df-ex 1538  df-nf 1540
 Copyright terms: Public domain W3C validator