Theorem bj-sbievw1

Description: Lemma for substitution. (Contributed by BJ, 23-Jul-2023)

	Ref	Expression
Assertion	bj-sbievw1	|- ( [ y / x ] ( ph -> ps ) -> ( [ y / x ] ph -> ps ) )

Proof

Step	Hyp	Ref	Expression
1		sb6	|- ( [ y / x ] ( ph -> ps ) <-> A. x ( x = y -> ( ph -> ps ) ) )
2		bj-sblem1	|- ( A. x ( x = y -> ( ph -> ps ) ) -> ( A. x ( x = y -> ph ) -> ( E. x x = y -> ps ) ) )
3		sb6	|- ( [ y / x ] ph <-> A. x ( x = y -> ph ) )
4		ax6ev	|- E. x x = y
5	4	a1bi	|- ( ps <-> ( E. x x = y -> ps ) )
6	2 3 5	3imtr4g	|- ( A. x ( x = y -> ( ph -> ps ) ) -> ( [ y / x ] ph -> ps ) )
7	1 6	sylbi	|- ( [ y / x ] ( ph -> ps ) -> ( [ y / x ] ph -> ps ) )