Theorem sb9

Description: Commutation of quantification and substitution variables. Usage of this theorem is discouraged because it depends on ax-13 . (Contributed by NM, 5-Aug-1993) Allow a shortening of sb9i . (Revised by Wolf Lammen, 15-Jun-2019) (New usage is discouraged.)

	Ref	Expression
Assertion	sb9	$$⊢\forall x\left[x/y\right]\phi \leftrightarrow \forall y\left[y/x\right]\phi$$

Proof

Step	Hyp	Ref	Expression
1		sbequ12a	$$⊢y=x\to \left(\left[x/y\right]\phi \leftrightarrow \left[y/x\right]\phi \right)$$
2	1	equcoms	$$⊢x=y\to \left(\left[x/y\right]\phi \leftrightarrow \left[y/x\right]\phi \right)$$
3	2	sps	$$⊢\forall xx=y\to \left(\left[x/y\right]\phi \leftrightarrow \left[y/x\right]\phi \right)$$
4	3	dral1	$$⊢\forall xx=y\to \left(\forall x\left[x/y\right]\phi \leftrightarrow \forall y\left[y/x\right]\phi \right)$$
5		nfnae	$$⊢Ⅎx\neg \forall xx=y$$
6		nfnae	$$⊢Ⅎy\neg \forall xx=y$$
7		nfsb2	$$⊢\neg \forall yy=x\to Ⅎy\left[x/y\right]\phi$$
8	7	naecoms	$$⊢\neg \forall xx=y\to Ⅎy\left[x/y\right]\phi$$
9		nfsb2	$$⊢\neg \forall xx=y\to Ⅎx\left[y/x\right]\phi$$
10	2	a1i	$$⊢\neg \forall xx=y\to \left(x=y\to \left(\left[x/y\right]\phi \leftrightarrow \left[y/x\right]\phi \right)\right)$$
11	5 6 8 9 10	cbv2	$$⊢\neg \forall xx=y\to \left(\forall x\left[x/y\right]\phi \leftrightarrow \forall y\left[y/x\right]\phi \right)$$
12	4 11	pm2.61i	$$⊢\forall x\left[x/y\right]\phi \leftrightarrow \forall y\left[y/x\right]\phi$$