Theorem exnelv

Description: For any set x , there is a set not contained in x . The proof is based on Russell's paradox. (Contributed by NM, 23-Aug-1993) Remove use of ax-12 and ax-13 . (Revised by BJ, 31-May-2019) Extract from nalset . (Revised by Matthew House, 12-Apr-2026)

	Ref	Expression
Assertion	exnelv	|- E. y -. y e. x

Proof

Step	Hyp	Ref	Expression
1		ax-sep	|- E. y A. z ( z e. y <-> ( z e. x /\ -. z e. z ) )
2		elequ1	|- ( z = y -> ( z e. x <-> y e. x ) )
3		elequ2	|- ( z = y -> ( z e. z <-> z e. y ) )
4	3	notbid	|- ( z = y -> ( -. z e. z <-> -. z e. y ) )
5	2 4	anbi12d	|- ( z = y -> ( ( z e. x /\ -. z e. z ) <-> ( y e. x /\ -. z e. y ) ) )
6	5	bibi2d	|- ( z = y -> ( ( z e. y <-> ( z e. x /\ -. z e. z ) ) <-> ( z e. y <-> ( y e. x /\ -. z e. y ) ) ) )
7		pclem6	|- ( ( z e. y <-> ( y e. x /\ -. z e. y ) ) -> -. y e. x )
8	6 7	biimtrdi	|- ( z = y -> ( ( z e. y <-> ( z e. x /\ -. z e. z ) ) -> -. y e. x ) )
9	8	spimvw	|- ( A. z ( z e. y <-> ( z e. x /\ -. z e. z ) ) -> -. y e. x )
10	1 9	eximii	|- E. y -. y e. x