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	$$⊢\exists y\neg y\in x$$

Proof

Step	Hyp	Ref	Expression
1		ax-sep	$$⊢\exists y\forall z\left(z\in y\leftrightarrow \left(z\in x\wedge \neg z\in z\right)\right)$$
2		elequ1	$$⊢z=y\to \left(z\in x\leftrightarrow y\in x\right)$$
3		elequ2	$$⊢z=y\to \left(z\in z\leftrightarrow z\in y\right)$$
4	3	notbid	$$⊢z=y\to \left(\neg z\in z\leftrightarrow \neg z\in y\right)$$
5	2 4	anbi12d	$$⊢z=y\to \left(\left(z\in x\wedge \neg z\in z\right)\leftrightarrow \left(y\in x\wedge \neg z\in y\right)\right)$$
6	5	bibi2d	$$⊢z=y\to \left(\left(z\in y\leftrightarrow \left(z\in x\wedge \neg z\in z\right)\right)\leftrightarrow \left(z\in y\leftrightarrow \left(y\in x\wedge \neg z\in y\right)\right)\right)$$
7		pclem6	$$⊢\left(z\in y\leftrightarrow \left(y\in x\wedge \neg z\in y\right)\right)\to \neg y\in x$$
8	6 7	biimtrdi	$$⊢z=y\to \left(\left(z\in y\leftrightarrow \left(z\in x\wedge \neg z\in z\right)\right)\to \neg y\in x\right)$$
9	8	spimvw	$$⊢\forall z\left(z\in y\leftrightarrow \left(z\in x\wedge \neg z\in z\right)\right)\to \neg y\in x$$
10	1 9	eximii	$$⊢\exists y\neg y\in x$$