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