Description: An equation between setvar is free of any other setvar. Usage of this theorem is discouraged because it depends on ax-13 . (Contributed by Wolf Lammen, 9-Jun-2019) Remove dependency on ax-12 . (Revised by Wolf Lammen, 16-Dec-2022) (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | nfeqf2 | ⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → Ⅎ 𝑥 𝑧 = 𝑦 ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | exnal | ⊢ ( ∃ 𝑥 ¬ 𝑥 = 𝑦 ↔ ¬ ∀ 𝑥 𝑥 = 𝑦 ) | |
| 2 | hbe1 | ⊢ ( ∃ 𝑥 𝑧 = 𝑦 → ∀ 𝑥 ∃ 𝑥 𝑧 = 𝑦 ) | |
| 3 | ax13lem2 | ⊢ ( ¬ 𝑥 = 𝑦 → ( ∃ 𝑥 𝑧 = 𝑦 → 𝑧 = 𝑦 ) ) | |
| 4 | ax13lem1 | ⊢ ( ¬ 𝑥 = 𝑦 → ( 𝑧 = 𝑦 → ∀ 𝑥 𝑧 = 𝑦 ) ) | |
| 5 | 3 4 | syldc | ⊢ ( ∃ 𝑥 𝑧 = 𝑦 → ( ¬ 𝑥 = 𝑦 → ∀ 𝑥 𝑧 = 𝑦 ) ) |
| 6 | 2 5 | eximdh | ⊢ ( ∃ 𝑥 𝑧 = 𝑦 → ( ∃ 𝑥 ¬ 𝑥 = 𝑦 → ∃ 𝑥 ∀ 𝑥 𝑧 = 𝑦 ) ) |
| 7 | hbe1a | ⊢ ( ∃ 𝑥 ∀ 𝑥 𝑧 = 𝑦 → ∀ 𝑥 𝑧 = 𝑦 ) | |
| 8 | 6 7 | syl6com | ⊢ ( ∃ 𝑥 ¬ 𝑥 = 𝑦 → ( ∃ 𝑥 𝑧 = 𝑦 → ∀ 𝑥 𝑧 = 𝑦 ) ) |
| 9 | 8 | nfd | ⊢ ( ∃ 𝑥 ¬ 𝑥 = 𝑦 → Ⅎ 𝑥 𝑧 = 𝑦 ) |
| 10 | 1 9 | sylbir | ⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → Ⅎ 𝑥 𝑧 = 𝑦 ) |