Theorem bj-ru1

Description: A version of Russell's paradox ru (see also bj-ru ). (Contributed by BJ, 12-Oct-2019) (Proof modification is discouraged.)

	Ref	Expression
Assertion	bj-ru1	$$⊢\neg \exists yy=\left\{x|\neg x\in x\right\}$$

Proof

Step	Hyp	Ref	Expression
1		bj-ru0	$$⊢\neg \forall x\left(x\in y\leftrightarrow \neg x\in x\right)$$
2		abeq2	$$⊢y=\left\{x|\neg x\in x\right\}\leftrightarrow \forall x\left(x\in y\leftrightarrow \neg x\in x\right)$$
3	1 2	mtbir	$$⊢\neg y=\left\{x|\neg x\in x\right\}$$
4	3	nex	$$⊢\neg \exists yy=\left\{x|\neg x\in x\right\}$$