Theorem wl-19.8eqv

Description: Under the assumption -. x = y a specialized version of 19.8a is provable from Tarski's FOL and ax13v only. Note that this reverts the implication in ax13lem2 , so in fact ( -. x = y -> ( E. x z = y <-> z = y ) ) holds. (Contributed by Wolf Lammen, 17-Apr-2021)

	Ref	Expression
Assertion	wl-19.8eqv	$$⊢\neg x=y\to \left(z=y\to \exists xz=y\right)$$

Proof

Step	Hyp	Ref	Expression
1		ax13lem1	$$⊢\neg x=y\to \left(z=y\to \forall xz=y\right)$$
2		19.2	$$⊢\forall xz=y\to \exists xz=y$$
3	1 2	syl6	$$⊢\neg x=y\to \left(z=y\to \exists xz=y\right)$$