This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ruOLD

Description: Obsolete version of ru as of 20-Jun-2025. (Contributed by NM, 7-Aug-1994) Remove use of ax-13 . (Revised by BJ, 12-Oct-2019) (Proof modification is discouraged.) (New usage is discouraged.)

		Ref	Expression
	Assertion	ruOLD	$⊢ \{x \| x \notin x\} \notin V$

Proof

Step	Hyp	Ref	Expression
1		pm5.19	$⊢ \neg (y \in y \leftrightarrow \neg y \in y)$
2		eleq1w	$⊢ x = y \to (x \in y \leftrightarrow y \in y)$
3		df-nel	$⊢ x \notin x \leftrightarrow \neg x \in x$
4		id	$⊢ x = y \to x = y$
5	4 4	eleq12d	$⊢ x = y \to (x \in x \leftrightarrow y \in y)$
6	5	notbid	$⊢ x = y \to (\neg x \in x \leftrightarrow \neg y \in y)$
7	3 6	bitrid	$⊢ x = y \to (x \notin x \leftrightarrow \neg y \in y)$
8	2 7	bibi12d	$⊢ x = y \to ((x \in y \leftrightarrow x \notin x) \leftrightarrow (y \in y \leftrightarrow \neg y \in y))$
9	8	spvv	$⊢ \forall x (x \in y \leftrightarrow x \notin x) \to (y \in y \leftrightarrow \neg y \in y)$
10	1 9	mto	$⊢ \neg \forall x (x \in y \leftrightarrow x \notin x)$
11		eqabb	$⊢ y = \{x \| x \notin x\} \leftrightarrow \forall x (x \in y \leftrightarrow x \notin x)$
12	10 11	mtbir	$⊢ \neg y = \{x \| x \notin x\}$
13	12	nex	$⊢ \neg \exists y y = \{x \| x \notin x\}$
14		isset	$⊢ \{x \| x \notin x\} \in V \leftrightarrow \exists y y = \{x \| x \notin x\}$
15	13 14	mtbir	$⊢ \neg \{x \| x \notin x\} \in V$
16	15	nelir	$⊢ \{x \| x \notin x\} \notin V$