Theorem wl-sbcom2d-lem2

Description: Lemma used to prove wl-sbcom2d . (Contributed by Wolf Lammen, 10-Aug-2019) (New usage is discouraged.)

	Ref	Expression
Assertion	wl-sbcom2d-lem2	$$⊢\neg \forall yy=x\to \left(\left[u/x\right]\left[v/y\right]\phi \leftrightarrow \forall x\forall y\left(\left(x=u\wedge y=v\right)\to \phi \right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		id	$$⊢\neg \forall yy=x\to \neg \forall yy=x$$
2		naev	$$⊢\neg \forall yy=x\to \neg \forall yy=v$$
3		naev	$$⊢\neg \forall yy=x\to \neg \forall yy=u$$
4		naev	$$⊢\neg \forall yy=x\to \neg \forall xx=u$$
5	1 2 3 4	wl-2sb6d	$$⊢\neg \forall yy=x\to \left(\left[u/x\right]\left[v/y\right]\phi \leftrightarrow \forall x\forall y\left(\left(x=u\wedge y=v\right)\to \phi \right)\right)$$