Metamath Proof Explorer


Theorem nalset

Description: No set contains all sets. Theorem 41 of Suppes p. 30. (Contributed by NM, 23-Aug-1993) Remove use of ax-12 and ax-13 . (Revised by BJ, 31-May-2019)

Ref Expression
Assertion nalset
|- -. E. x A. y y e. x

Proof

Step Hyp Ref Expression
1 alexn
 |-  ( A. x E. y -. y e. x <-> -. E. x A. y y e. x )
2 ax-sep
 |-  E. y A. z ( z e. y <-> ( z e. x /\ -. z e. z ) )
3 elequ1
 |-  ( z = y -> ( z e. y <-> y e. y ) )
4 elequ1
 |-  ( z = y -> ( z e. x <-> y e. x ) )
5 elequ1
 |-  ( z = y -> ( z e. z <-> y e. z ) )
6 elequ2
 |-  ( z = y -> ( y e. z <-> y e. y ) )
7 5 6 bitrd
 |-  ( z = y -> ( z e. z <-> y e. y ) )
8 7 notbid
 |-  ( z = y -> ( -. z e. z <-> -. y e. y ) )
9 4 8 anbi12d
 |-  ( z = y -> ( ( z e. x /\ -. z e. z ) <-> ( y e. x /\ -. y e. y ) ) )
10 3 9 bibi12d
 |-  ( z = y -> ( ( z e. y <-> ( z e. x /\ -. z e. z ) ) <-> ( y e. y <-> ( y e. x /\ -. y e. y ) ) ) )
11 10 spvv
 |-  ( A. z ( z e. y <-> ( z e. x /\ -. z e. z ) ) -> ( y e. y <-> ( y e. x /\ -. y e. y ) ) )
12 pclem6
 |-  ( ( y e. y <-> ( y e. x /\ -. y e. y ) ) -> -. y e. x )
13 11 12 syl
 |-  ( A. z ( z e. y <-> ( z e. x /\ -. z e. z ) ) -> -. y e. x )
14 2 13 eximii
 |-  E. y -. y e. x
15 1 14 mpgbi
 |-  -. E. x A. y y e. x