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	$$⊢\neg x=y\to \left(\exists xz=y\to z=y\right)$$

Proof

Step	Hyp	Ref	Expression
1		ax13lem1	$$⊢\neg x=y\to \left(w=y\to \forall xw=y\right)$$
2		equeucl	$$⊢z=y\to \left(w=y\to z=w\right)$$
3	2	eximi	$$⊢\exists xz=y\to \exists x\left(w=y\to z=w\right)$$
4		19.36v	$$⊢\exists x\left(w=y\to z=w\right)\leftrightarrow \left(\forall xw=y\to z=w\right)$$
5	3 4	sylib	$$⊢\exists xz=y\to \left(\forall xw=y\to z=w\right)$$
6	1 5	syl9	$$⊢\neg x=y\to \left(\exists xz=y\to \left(w=y\to z=w\right)\right)$$
7	6	alrimdv	$$⊢\neg x=y\to \left(\exists xz=y\to \forall w\left(w=y\to z=w\right)\right)$$
8		equequ2	$$⊢w=y\to \left(z=w\leftrightarrow z=y\right)$$
9	8	equsalvw	$$⊢\forall w\left(w=y\to z=w\right)\leftrightarrow z=y$$
10	7 9	syl6ib	$$⊢\neg x=y\to \left(\exists xz=y\to z=y\right)$$