Metamath Proof Explorer


Theorem ax13lem2

Description: Lemma for nfeqf2 . This lemma is equivalent to ax13v with one distinct variable constraint removed. (Contributed by Wolf Lammen, 8-Sep-2018) Reduce axiom usage. (Revised by Wolf Lammen, 18-Oct-2020) (New usage is discouraged.)

Ref Expression
Assertion ax13lem2 ( ¬ 𝑥 = 𝑦 → ( ∃ 𝑥 𝑧 = 𝑦𝑧 = 𝑦 ) )

Proof

Step Hyp Ref Expression
1 ax13lem1 ( ¬ 𝑥 = 𝑦 → ( 𝑤 = 𝑦 → ∀ 𝑥 𝑤 = 𝑦 ) )
2 equeucl ( 𝑧 = 𝑦 → ( 𝑤 = 𝑦𝑧 = 𝑤 ) )
3 2 eximi ( ∃ 𝑥 𝑧 = 𝑦 → ∃ 𝑥 ( 𝑤 = 𝑦𝑧 = 𝑤 ) )
4 19.36v ( ∃ 𝑥 ( 𝑤 = 𝑦𝑧 = 𝑤 ) ↔ ( ∀ 𝑥 𝑤 = 𝑦𝑧 = 𝑤 ) )
5 3 4 sylib ( ∃ 𝑥 𝑧 = 𝑦 → ( ∀ 𝑥 𝑤 = 𝑦𝑧 = 𝑤 ) )
6 1 5 syl9 ( ¬ 𝑥 = 𝑦 → ( ∃ 𝑥 𝑧 = 𝑦 → ( 𝑤 = 𝑦𝑧 = 𝑤 ) ) )
7 6 alrimdv ( ¬ 𝑥 = 𝑦 → ( ∃ 𝑥 𝑧 = 𝑦 → ∀ 𝑤 ( 𝑤 = 𝑦𝑧 = 𝑤 ) ) )
8 equequ2 ( 𝑤 = 𝑦 → ( 𝑧 = 𝑤𝑧 = 𝑦 ) )
9 8 equsalvw ( ∀ 𝑤 ( 𝑤 = 𝑦𝑧 = 𝑤 ) ↔ 𝑧 = 𝑦 )
10 7 9 syl6ib ( ¬ 𝑥 = 𝑦 → ( ∃ 𝑥 𝑧 = 𝑦𝑧 = 𝑦 ) )