Theorem wl-equsb3

Description: equsb3 with a distinctor. (Contributed by Wolf Lammen, 27-Jun-2019)

	Ref	Expression
Assertion	wl-equsb3	$$⊢\neg \forall yy=z\to \left(\left[x/y\right]y=z\leftrightarrow x=z\right)$$

Proof

Step	Hyp	Ref	Expression
1		nfna1	$$⊢Ⅎy\neg \forall yy=z$$
2		nfeqf2	$$⊢\neg \forall yy=z\to Ⅎyw=z$$
3		equequ1	$$⊢y=w\to \left(y=z\leftrightarrow w=z\right)$$
4	3	a1i	$$⊢\neg \forall yy=z\to \left(y=w\to \left(y=z\leftrightarrow w=z\right)\right)$$
5	1 2 4	sbied	$$⊢\neg \forall yy=z\to \left(\left[w/y\right]y=z\leftrightarrow w=z\right)$$
6	5	sbbidv	$$⊢\neg \forall yy=z\to \left(\left[x/w\right]\left[w/y\right]y=z\leftrightarrow \left[x/w\right]w=z\right)$$
7		sbco2vv	$$⊢\left[x/w\right]\left[w/y\right]y=z\leftrightarrow \left[x/y\right]y=z$$
8		equsb3	$$⊢\left[x/w\right]w=z\leftrightarrow x=z$$
9	6 7 8	3bitr3g	$$⊢\neg \forall yy=z\to \left(\left[x/y\right]y=z\leftrightarrow x=z\right)$$