Theorem wl-ax11-lem4

Description: Lemma. (Contributed by Wolf Lammen, 30-Jun-2019)

	Ref	Expression
Assertion	wl-ax11-lem4	$$⊢Ⅎx\left(\forall uu=y\wedge \neg \forall xx=y\right)$$

Proof

Step	Hyp	Ref	Expression
1		ancom	$$⊢\left(\forall uu=y\wedge \neg \forall xx=y\right)\leftrightarrow \left(\neg \forall xx=y\wedge \forall uu=y\right)$$
2		nfna1	$$⊢Ⅎx\neg \forall xx=y$$
3		wl-ax11-lem3	$$⊢\neg \forall xx=y\to Ⅎx\forall uu=y$$
4	2 3	nfan1	$$⊢Ⅎx\left(\neg \forall xx=y\wedge \forall uu=y\right)$$
5	1 4	nfxfr	$$⊢Ⅎx\left(\forall uu=y\wedge \neg \forall xx=y\right)$$