This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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