Theorem nfsb4t

Description: A variable not free in a proposition remains so after substitution in that proposition with a distinct variable (closed form of nfsb4 ). Usage of this theorem is discouraged because it depends on ax-13 . (Contributed by NM, 7-Apr-2004) (Revised by Mario Carneiro, 4-Oct-2016) (Proof shortened by Wolf Lammen, 11-May-2018) (New usage is discouraged.)

	Ref	Expression
Assertion	nfsb4t	$$⊢\forall xℲz\phi \to \left(\neg \forall zz=y\to Ⅎz\left[y/x\right]\phi \right)$$

Proof

Step	Hyp	Ref	Expression
1		sbequ12	$$⊢x=y\to \left(\phi \leftrightarrow \left[y/x\right]\phi \right)$$
2	1	sps	$$⊢\forall xx=y\to \left(\phi \leftrightarrow \left[y/x\right]\phi \right)$$
3	2	drnf2	$$⊢\forall xx=y\to \left(Ⅎz\phi \leftrightarrow Ⅎz\left[y/x\right]\phi \right)$$
4	3	biimpd	$$⊢\forall xx=y\to \left(Ⅎz\phi \to Ⅎz\left[y/x\right]\phi \right)$$
5	4	spsd	$$⊢\forall xx=y\to \left(\forall xℲz\phi \to Ⅎz\left[y/x\right]\phi \right)$$
6	5	impcom	$$⊢\left(\forall xℲz\phi \wedge \forall xx=y\right)\to Ⅎz\left[y/x\right]\phi$$
7	6	a1d	$$⊢\left(\forall xℲz\phi \wedge \forall xx=y\right)\to \left(\neg \forall zz=y\to Ⅎz\left[y/x\right]\phi \right)$$
8		nfnf1	$$⊢ℲzℲz\phi$$
9	8	nfal	$$⊢Ⅎz\forall xℲz\phi$$
10		nfnae	$$⊢Ⅎz\neg \forall xx=y$$
11	9 10	nfan	$$⊢Ⅎz\left(\forall xℲz\phi \wedge \neg \forall xx=y\right)$$
12		nfa1	$$⊢Ⅎx\forall xℲz\phi$$
13		nfnae	$$⊢Ⅎx\neg \forall xx=y$$
14	12 13	nfan	$$⊢Ⅎx\left(\forall xℲz\phi \wedge \neg \forall xx=y\right)$$
15		sp	$$⊢\forall xℲz\phi \to Ⅎz\phi$$
16	15	adantr	$$⊢\left(\forall xℲz\phi \wedge \neg \forall xx=y\right)\to Ⅎz\phi$$
17		nfsb2	$$⊢\neg \forall xx=y\to Ⅎx\left[y/x\right]\phi$$
18	17	adantl	$$⊢\left(\forall xℲz\phi \wedge \neg \forall xx=y\right)\to Ⅎx\left[y/x\right]\phi$$
19	1	a1i	$$⊢\left(\forall xℲz\phi \wedge \neg \forall xx=y\right)\to \left(x=y\to \left(\phi \leftrightarrow \left[y/x\right]\phi \right)\right)$$
20	11 14 16 18 19	dvelimdf	$$⊢\left(\forall xℲz\phi \wedge \neg \forall xx=y\right)\to \left(\neg \forall zz=y\to Ⅎz\left[y/x\right]\phi \right)$$
21	7 20	pm2.61dan	$$⊢\forall xℲz\phi \to \left(\neg \forall zz=y\to Ⅎz\left[y/x\right]\phi \right)$$