This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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