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