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	$$⊢\left\{x|x\notin x\right\}\notin \mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		pm5.19	$$⊢\neg \left(y\in y\leftrightarrow \neg y\in y\right)$$
2		eleq1w	$$⊢x=y\to \left(x\in y\leftrightarrow y\in y\right)$$
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 \left(x\in x\leftrightarrow y\in y\right)$$
6	5	notbid	$$⊢x=y\to \left(\neg x\in x\leftrightarrow \neg y\in y\right)$$
7	3 6	bitrid	$$⊢x=y\to \left(x\notin x\leftrightarrow \neg y\in y\right)$$
8	2 7	bibi12d	$$⊢x=y\to \left(\left(x\in y\leftrightarrow x\notin x\right)\leftrightarrow \left(y\in y\leftrightarrow \neg y\in y\right)\right)$$
9	8	spvv	$$⊢\forall x\left(x\in y\leftrightarrow x\notin x\right)\to \left(y\in y\leftrightarrow \neg y\in y\right)$$
10	1 9	mto	$$⊢\neg \forall x\left(x\in y\leftrightarrow x\notin x\right)$$
11		eqabb	$$⊢y=\left\{x|x\notin x\right\}\leftrightarrow \forall x\left(x\in y\leftrightarrow x\notin x\right)$$
12	10 11	mtbir	$$⊢\neg y=\left\{x|x\notin x\right\}$$
13	12	nex	$$⊢\neg \exists yy=\left\{x|x\notin x\right\}$$
14		isset	$$⊢\left\{x|x\notin x\right\}\in \mathrm{V}\leftrightarrow \exists yy=\left\{x|x\notin x\right\}$$
15	13 14	mtbir	$$⊢\neg \left\{x|x\notin x\right\}\in \mathrm{V}$$
16	15	nelir	$$⊢\left\{x|x\notin x\right\}\notin \mathrm{V}$$