Theorem wl-19.2reqv

Description: Under the assumption -. x = y the reverse direction of 19.2 is provable from Tarski's FOL and ax13v only. Note that in conjunction with 19.2 in fact ( -. x = y -> ( A. x z = y <-> E. x z = y ) ) holds. (Contributed by Wolf Lammen, 17-Apr-2021)

	Ref	Expression
Assertion	wl-19.2reqv	⊢ ( ¬ 𝑥 = 𝑦 → ( ∃ 𝑥 𝑧 = 𝑦 → ∀ 𝑥 𝑧 = 𝑦 ) )

Proof

Step	Hyp	Ref	Expression
1		ax13lem2	⊢ ( ¬ 𝑥 = 𝑦 → ( ∃ 𝑥 𝑧 = 𝑦 → 𝑧 = 𝑦 ) )
2		ax13lem1	⊢ ( ¬ 𝑥 = 𝑦 → ( 𝑧 = 𝑦 → ∀ 𝑥 𝑧 = 𝑦 ) )
3	1 2	syld	⊢ ( ¬ 𝑥 = 𝑦 → ( ∃ 𝑥 𝑧 = 𝑦 → ∀ 𝑥 𝑧 = 𝑦 ) )