Theorem wl-ax11-lem6

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

	Ref	Expression
Assertion	wl-ax11-lem6	$$⊢\left(\forall uu=y\wedge \neg \forall xx=y\right)\to \left(\forall u\forall x\left[u/y\right]\phi \leftrightarrow \forall x\forall y\phi \right)$$

Proof

Step	Hyp	Ref	Expression
1		ax-wl-11v	$$⊢\forall u\forall x\left[u/y\right]\phi \to \forall x\forall u\left[u/y\right]\phi$$
2		ax-wl-11v	$$⊢\forall x\forall u\left[u/y\right]\phi \to \forall u\forall x\left[u/y\right]\phi$$
3	1 2	impbii	$$⊢\forall u\forall x\left[u/y\right]\phi \leftrightarrow \forall x\forall u\left[u/y\right]\phi$$
4		nfna1	$$⊢Ⅎx\neg \forall xx=y$$
5		wl-ax11-lem3	$$⊢\neg \forall xx=y\to Ⅎx\forall uu=y$$
6	4 5	nfan1	$$⊢Ⅎx\left(\neg \forall xx=y\wedge \forall uu=y\right)$$
7		wl-ax11-lem5	$$⊢\forall uu=y\to \left(\forall u\left[u/y\right]\phi \leftrightarrow \forall y\phi \right)$$
8	7	adantl	$$⊢\left(\neg \forall xx=y\wedge \forall uu=y\right)\to \left(\forall u\left[u/y\right]\phi \leftrightarrow \forall y\phi \right)$$
9	6 8	albid	$$⊢\left(\neg \forall xx=y\wedge \forall uu=y\right)\to \left(\forall x\forall u\left[u/y\right]\phi \leftrightarrow \forall x\forall y\phi \right)$$
10	9	ancoms	$$⊢\left(\forall uu=y\wedge \neg \forall xx=y\right)\to \left(\forall x\forall u\left[u/y\right]\phi \leftrightarrow \forall x\forall y\phi \right)$$
11	3 10	bitrid	$$⊢\left(\forall uu=y\wedge \neg \forall xx=y\right)\to \left(\forall u\forall x\left[u/y\right]\phi \leftrightarrow \forall x\forall y\phi \right)$$