Theorem exnel

Description: There is always a set not in y . (Contributed by Scott Fenton, 13-Dec-2010)

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

Proof

Step	Hyp	Ref	Expression
1		elirrv	|- -. y e. y
2	1	nfth	|- F/ x -. y e. y
3		ax8	|- ( x = y -> ( x e. y -> y e. y ) )
4	3	con3d	|- ( x = y -> ( -. y e. y -> -. x e. y ) )
5	2 4	spime	|- ( -. y e. y -> E. x -. x e. y )
6	1 5	ax-mp	|- E. x -. x e. y