Metamath Proof Explorer


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 ¬ x x y ¬ x x

Proof

Step Hyp Ref Expression
1 pm5.19 ¬ y y ¬ y y
2 elequ1 x = y x y y y
3 elequ12 x = y x = y x x y y
4 3 anidms x = y x x y y
5 4 notbid x = y ¬ x x ¬ y y
6 2 5 bibi12d x = y x y ¬ x x y y ¬ y y
7 6 spvv x x y ¬ x x y y ¬ y y
8 1 7 mto ¬ x x y ¬ x x