Description: A version of ax13v with one distinct variable restriction dropped. For convenience, y is kept on the right side of equations. The proof of ax13 bases on ideas from NM, 24-Dec-2015. (Contributed by Wolf Lammen, 8-Sep-2018) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Assertion | ax13lem1 | ⊢ ( ¬ 𝑥 = 𝑦 → ( 𝑧 = 𝑦 → ∀ 𝑥 𝑧 = 𝑦 ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | equvinva | ⊢ ( 𝑧 = 𝑦 → ∃ 𝑤 ( 𝑧 = 𝑤 ∧ 𝑦 = 𝑤 ) ) | |
2 | ax13v | ⊢ ( ¬ 𝑥 = 𝑦 → ( 𝑦 = 𝑤 → ∀ 𝑥 𝑦 = 𝑤 ) ) | |
3 | equeucl | ⊢ ( 𝑧 = 𝑤 → ( 𝑦 = 𝑤 → 𝑧 = 𝑦 ) ) | |
4 | 3 | alimdv | ⊢ ( 𝑧 = 𝑤 → ( ∀ 𝑥 𝑦 = 𝑤 → ∀ 𝑥 𝑧 = 𝑦 ) ) |
5 | 2 4 | syl9 | ⊢ ( ¬ 𝑥 = 𝑦 → ( 𝑧 = 𝑤 → ( 𝑦 = 𝑤 → ∀ 𝑥 𝑧 = 𝑦 ) ) ) |
6 | 5 | impd | ⊢ ( ¬ 𝑥 = 𝑦 → ( ( 𝑧 = 𝑤 ∧ 𝑦 = 𝑤 ) → ∀ 𝑥 𝑧 = 𝑦 ) ) |
7 | 6 | exlimdv | ⊢ ( ¬ 𝑥 = 𝑦 → ( ∃ 𝑤 ( 𝑧 = 𝑤 ∧ 𝑦 = 𝑤 ) → ∀ 𝑥 𝑧 = 𝑦 ) ) |
8 | 1 7 | syl5 | ⊢ ( ¬ 𝑥 = 𝑦 → ( 𝑧 = 𝑦 → ∀ 𝑥 𝑧 = 𝑦 ) ) |