Theorem exnel

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

	Ref	Expression
Assertion	exnel	$$⊢\exists x\neg x\in y$$

Proof

Step	Hyp	Ref	Expression
1		elirrv	$$⊢\neg y\in y$$
2	1	nfth	$$⊢Ⅎx\neg y\in y$$
3		ax8	$$⊢x=y\to \left(x\in y\to y\in y\right)$$
4	3	con3d	$$⊢x=y\to \left(\neg y\in y\to \neg x\in y\right)$$
5	2 4	spime	$$⊢\neg y\in y\to \exists x\neg x\in y$$
6	1 5	ax-mp	$$⊢\exists x\neg x\in y$$