Theorem hbsbw

Description: If z is not free in ph , it is not free in [ y / x ] ph when y and z are distinct. Version of hbsb with a disjoint variable condition, which requires fewer axioms. (Contributed by NM, 12-Aug-1993) (Revised by Gino Giotto, 23-May-2024)

	Ref	Expression
Hypothesis	hbsbw.1	$$⊢\phi \to \forall z\phi$$
Assertion	hbsbw	$$⊢\left[y/x\right]\phi \to \forall z\left[y/x\right]\phi$$

Proof

Step	Hyp	Ref	Expression
1		hbsbw.1	$$⊢\phi \to \forall z\phi$$
2		df-sb	$$⊢\left[y/x\right]\phi \leftrightarrow \forall w\left(w=y\to \forall x\left(x=w\to \phi \right)\right)$$
3	1	imim2i	$$⊢\left(x=w\to \phi \right)\to \left(x=w\to \forall z\phi \right)$$
4	3	alimi	$$⊢\forall x\left(x=w\to \phi \right)\to \forall x\left(x=w\to \forall z\phi \right)$$
5		19.21v	$$⊢\forall z\left(x=w\to \phi \right)\leftrightarrow \left(x=w\to \forall z\phi \right)$$
6	5	biimpri	$$⊢\left(x=w\to \forall z\phi \right)\to \forall z\left(x=w\to \phi \right)$$
7	6	alimi	$$⊢\forall x\left(x=w\to \forall z\phi \right)\to \forall x\forall z\left(x=w\to \phi \right)$$
8		ax-11	$$⊢\forall x\forall z\left(x=w\to \phi \right)\to \forall z\forall x\left(x=w\to \phi \right)$$
9	4 7 8	3syl	$$⊢\forall x\left(x=w\to \phi \right)\to \forall z\forall x\left(x=w\to \phi \right)$$
10	9	imim2i	$$⊢\left(w=y\to \forall x\left(x=w\to \phi \right)\right)\to \left(w=y\to \forall z\forall x\left(x=w\to \phi \right)\right)$$
11		19.21v	$$⊢\forall z\left(w=y\to \forall x\left(x=w\to \phi \right)\right)\leftrightarrow \left(w=y\to \forall z\forall x\left(x=w\to \phi \right)\right)$$
12	10 11	sylibr	$$⊢\left(w=y\to \forall x\left(x=w\to \phi \right)\right)\to \forall z\left(w=y\to \forall x\left(x=w\to \phi \right)\right)$$
13	12	hbal	$$⊢\forall w\left(w=y\to \forall x\left(x=w\to \phi \right)\right)\to \forall z\forall w\left(w=y\to \forall x\left(x=w\to \phi \right)\right)$$
14	2 13	hbxfrbi	$$⊢\left[y/x\right]\phi \to \forall z\left[y/x\right]\phi$$