Theorem bj-ru0

Description: The FOL part of Russell's paradox ru (see also bj-ru1 , bj-ru ). Use of elequ1 , bj-elequ12 (instead of eleq1 , eleq12d as in ru ) permits to remove dependency on ax-10 , ax-11 , ax-12 , ax-ext , df-sb , df-clab , df-cleq , df-clel . (Contributed by BJ, 12-Oct-2019) (Proof modification is discouraged.)

	Ref	Expression
Assertion	bj-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		bj-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)$$