Theorem hbsbwOLD

Description: Obsolete version of hbsbw as of 14-May-2025. (Contributed by NM, 12-Aug-1993) (Revised by GG, 23-May-2024) (New usage is discouraged.) (Proof modification is discouraged.)

	Ref	Expression
Hypothesis	hbsbw.1	|- ( ph -> A. z ph )
Assertion	hbsbwOLD	|- ( [ 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 )