Theorem ax13lem1

Description: A version of ax13v with one distinct variable restriction dropped. For convenience, y is kept on the right side of equations. The proof of ax13 bases on ideas from NM, 24-Dec-2015. (Contributed by Wolf Lammen, 8-Sep-2018) (New usage is discouraged.)

	Ref	Expression
Assertion	ax13lem1	$$⊢\neg x=y\to \left(z=y\to \forall xz=y\right)$$

Proof

Step	Hyp	Ref	Expression
1		equvinva	$$⊢z=y\to \exists w\left(z=w\wedge y=w\right)$$
2		ax13v	$$⊢\neg x=y\to \left(y=w\to \forall xy=w\right)$$
3		equeucl	$$⊢z=w\to \left(y=w\to z=y\right)$$
4	3	alimdv	$$⊢z=w\to \left(\forall xy=w\to \forall xz=y\right)$$
5	2 4	syl9	$$⊢\neg x=y\to \left(z=w\to \left(y=w\to \forall xz=y\right)\right)$$
6	5	impd	$$⊢\neg x=y\to \left(\left(z=w\wedge y=w\right)\to \forall xz=y\right)$$
7	6	exlimdv	$$⊢\neg x=y\to \left(\exists w\left(z=w\wedge y=w\right)\to \forall xz=y\right)$$
8	1 7	syl5	$$⊢\neg x=y\to \left(z=y\to \forall xz=y\right)$$