Theorem bj-sbievw

Description: Lemma for substitution. Closed form of equsalvw and sbievw . (Contributed by BJ, 23-Jul-2023)

	Ref	Expression
Assertion	bj-sbievw	|- ( [ 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-sblem	|- ( 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	3bitr4g	|- ( A. x ( x = y -> ( ph <-> ps ) ) -> ( [ y / x ] ph <-> ps ) )
7	1 6	sylbi	|- ( [ y / x ] ( ph <-> ps ) -> ( [ y / x ] ph <-> ps ) )