Theorem wl-ax13lem1

Description: A version of ax-wl-13v with one distinct variable restriction dropped. For convenience, y is kept on the right side of equations. This proof bases on ideas from NM, 24-Dec-2015. (Contributed by Wolf Lammen, 23-Jul-2021)

	Ref	Expression
Assertion	wl-ax13lem1	$$⊢\neg \forall xx=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		ax-wl-13v	$$⊢\neg \forall xx=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 \forall xx=y\to \left(z=w\to \left(y=w\to \forall xz=y\right)\right)$$
6	5	impd	$$⊢\neg \forall xx=y\to \left(\left(z=w\wedge y=w\right)\to \forall xz=y\right)$$
7	6	exlimdv	$$⊢\neg \forall xx=y\to \left(\exists w\left(z=w\wedge y=w\right)\to \forall xz=y\right)$$
8	1 7	syl5	$$⊢\neg \forall xx=y\to \left(z=y\to \forall xz=y\right)$$