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 ¬ ∀ 𝑥 ( 𝑥𝑦 ↔ ¬ 𝑥𝑥 )

Proof

Step Hyp Ref Expression
1 pm5.19 ¬ ( 𝑦𝑦 ↔ ¬ 𝑦𝑦 )
2 elequ1 ( 𝑥 = 𝑦 → ( 𝑥𝑦𝑦𝑦 ) )
3 elequ12 ( ( 𝑥 = 𝑦𝑥 = 𝑦 ) → ( 𝑥𝑥𝑦𝑦 ) )
4 3 anidms ( 𝑥 = 𝑦 → ( 𝑥𝑥𝑦𝑦 ) )
5 4 notbid ( 𝑥 = 𝑦 → ( ¬ 𝑥𝑥 ↔ ¬ 𝑦𝑦 ) )
6 2 5 bibi12d ( 𝑥 = 𝑦 → ( ( 𝑥𝑦 ↔ ¬ 𝑥𝑥 ) ↔ ( 𝑦𝑦 ↔ ¬ 𝑦𝑦 ) ) )
7 6 spvv ( ∀ 𝑥 ( 𝑥𝑦 ↔ ¬ 𝑥𝑥 ) → ( 𝑦𝑦 ↔ ¬ 𝑦𝑦 ) )
8 1 7 mto ¬ ∀ 𝑥 ( 𝑥𝑦 ↔ ¬ 𝑥𝑥 )