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	|- ( ph -> A. z ph )
Assertion	hbsbw	|- ( [ y / x ] ph -> A. z [ y / x ] ph )

Proof

Step	Hyp	Ref	Expression
1		hbsbw.1	|- ( ph -> A. z ph )
2		df-sb	|- ( [ y / x ] ph <-> A. w ( w = y -> A. x ( x = w -> ph ) ) )
3	1	imim2i	|- ( ( x = w -> ph ) -> ( x = w -> A. z ph ) )
4	3	alimi	|- ( A. x ( x = w -> ph ) -> A. x ( x = w -> A. z ph ) )
5		19.21v	|- ( A. z ( x = w -> ph ) <-> ( x = w -> A. z ph ) )
6	5	biimpri	|- ( ( x = w -> A. z ph ) -> A. z ( x = w -> ph ) )
7	6	alimi	|- ( A. x ( x = w -> A. z ph ) -> A. x A. z ( x = w -> ph ) )
8		ax-11	|- ( A. x A. z ( x = w -> ph ) -> A. z A. x ( x = w -> ph ) )
9	4 7 8	3syl	|- ( A. x ( x = w -> ph ) -> A. z A. x ( x = w -> ph ) )
10	9	imim2i	|- ( ( w = y -> A. x ( x = w -> ph ) ) -> ( w = y -> A. z A. x ( x = w -> ph ) ) )
11		19.21v	|- ( A. z ( w = y -> A. x ( x = w -> ph ) ) <-> ( w = y -> A. z A. x ( x = w -> ph ) ) )
12	10 11	sylibr	|- ( ( w = y -> A. x ( x = w -> ph ) ) -> A. z ( w = y -> A. x ( x = w -> ph ) ) )
13	12	hbal	|- ( A. w ( w = y -> A. x ( x = w -> ph ) ) -> A. z A. w ( w = y -> A. x ( x = w -> ph ) ) )
14	2 13	hbxfrbi	|- ( [ y / x ] ph -> A. z [ y / x ] ph )