Metamath Proof Explorer


Theorem ax13lem1

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 ( ¬ 𝑥 = 𝑦 → ( 𝑧 = 𝑦 → ∀ 𝑥 𝑧 = 𝑦 ) )

Proof

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 ( ¬ 𝑥 = 𝑦 → ( 𝑧 = 𝑦 → ∀ 𝑥 𝑧 = 𝑦 ) )