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 (z \in y \leftrightarrow (z \in x \land \neg z \in z))$
2		elequ1	$⊢ z = y \to (z \in x \leftrightarrow y \in x)$
3		elequ2	$⊢ z = y \to (z \in z \leftrightarrow z \in y)$
4	3	notbid	$⊢ z = y \to (\neg z \in z \leftrightarrow \neg z \in y)$
5	2 4	anbi12d	$⊢ z = y \to ((z \in x \land \neg z \in z) \leftrightarrow (y \in x \land \neg z \in y))$
6	5	bibi2d	$⊢ z = y \to ((z \in y \leftrightarrow (z \in x \land \neg z \in z)) \leftrightarrow (z \in y \leftrightarrow (y \in x \land \neg z \in y)))$
7		pclem6	$⊢ (z \in y \leftrightarrow (y \in x \land \neg z \in y)) \to \neg y \in x$
8	6 7	biimtrdi	$⊢ z = y \to ((z \in y \leftrightarrow (z \in x \land \neg z \in z)) \to \neg y \in x)$
9	8	spimvw	$⊢ \forall z (z \in y \leftrightarrow (z \in x \land \neg z \in z)) \to \neg y \in x$
10	1 9	eximii	$⊢ \exists y \neg y \in x$

Metamath Proof Explorer

Theorem exnelv

Proof