Theorem wl-euequf

Description: euequ proved with a distinctor. (Contributed by Wolf Lammen, 23-Sep-2020)

	Ref	Expression
Assertion	wl-euequf	$$⊢\neg \forall xx=y\to \exists !xx=y$$

Proof

Step	Hyp	Ref	Expression
1		ax6ev	$$⊢\exists zz=y$$
2		nfv	$$⊢Ⅎz\neg \forall xx=y$$
3		nfna1	$$⊢Ⅎx\neg \forall xx=y$$
4		nfeqf2	$$⊢\neg \forall xx=y\to Ⅎxz=y$$
5		equequ2	$$⊢y=z\to \left(x=y\leftrightarrow x=z\right)$$
6	5	equcoms	$$⊢z=y\to \left(x=y\leftrightarrow x=z\right)$$
7	6	a1i	$$⊢\neg \forall xx=y\to \left(z=y\to \left(x=y\leftrightarrow x=z\right)\right)$$
8	3 4 7	alrimdd	$$⊢\neg \forall xx=y\to \left(z=y\to \forall x\left(x=y\leftrightarrow x=z\right)\right)$$
9	2 8	eximd	$$⊢\neg \forall xx=y\to \left(\exists zz=y\to \exists z\forall x\left(x=y\leftrightarrow x=z\right)\right)$$
10	1 9	mpi	$$⊢\neg \forall xx=y\to \exists z\forall x\left(x=y\leftrightarrow x=z\right)$$
11		eu6	$$⊢\exists !xx=y\leftrightarrow \exists z\forall x\left(x=y\leftrightarrow x=z\right)$$
12	10 11	sylibr	$$⊢\neg \forall xx=y\to \exists !xx=y$$