Theorem ru0

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.)

Conclusion
\( \vdash \neg \forall x \, (x \in y' \leftrightarrow \neg x \in x) \)
Proof
l0
pm5.19
\( \vdash \neg (y' \in y' \leftrightarrow \neg y' \in y') \)
l1
elequ1
elequ12
anidms _
notbid _
bibi12d l1 _
\( \vdash x = y' \rightarrow (x \in y' \leftrightarrow \neg x \in x \leftrightarrow (y' \in y' \leftrightarrow \neg y' \in y')) \)
spvv _
\( \vdash \forall x \, (x \in y' \leftrightarrow \neg x \in x) \rightarrow (y' \in y' \leftrightarrow \neg y' \in y') \)
mto l0 _