Theorem ru0

Description: The FOL statement used in the standard proof of Russell's paradox ru . (Contributed by NM, 7-Aug-1994) Extract from proof of ru and reduce axiom usage. (Revised by BJ, 12-Oct-2019)

	Ref	Expression
Assertion	ru0	$$⊢\neg \forall x\left(x\in y\leftrightarrow \neg x\in x\right)$$

Proof

Step	Hyp	Ref	Expression
1		pm5.19	$$⊢\neg \left(y\in y\leftrightarrow \neg y\in y\right)$$
2		elequ1	$$⊢x=y\to \left(x\in y\leftrightarrow y\in y\right)$$
3		elequ12	$$⊢\left(x=y\wedge x=y\right)\to \left(x\in x\leftrightarrow y\in y\right)$$
4	3	anidms	$$⊢x=y\to \left(x\in x\leftrightarrow y\in y\right)$$
5	4	notbid	$$⊢x=y\to \left(\neg x\in x\leftrightarrow \neg y\in y\right)$$
6	2 5	bibi12d	$$⊢x=y\to \left(\left(x\in y\leftrightarrow \neg x\in x\right)\leftrightarrow \left(y\in y\leftrightarrow \neg y\in y\right)\right)$$
7	6	spvv	$$⊢\forall x\left(x\in y\leftrightarrow \neg x\in x\right)\to \left(y\in y\leftrightarrow \neg y\in y\right)$$
8	1 7	mto	$$⊢\neg \forall x\left(x\in y\leftrightarrow \neg x\in x\right)$$