Theorem bj-sbievv

Description: Version of sbie with a second nonfreeness hypothesis and shorter proof. (Contributed by BJ, 18-Jul-2023) (Proof modification is discouraged.)

	Ref	Expression
Hypotheses	bj-sbievv.nfx	|- F/ x ps
	bj-sbievv.nfy	|- F/ y ph
	bj-sbievv.is	|- ( x = y -> ( ph <-> ps ) )
Assertion	bj-sbievv	|- ( [ y / x ] ph <-> ps )

Proof

Step	Hyp	Ref	Expression
1		bj-sbievv.nfx	|- F/ x ps
2		bj-sbievv.nfy	|- F/ y ph
3		bj-sbievv.is	|- ( x = y -> ( ph <-> ps ) )
4	2	sb6f	|- ( [ y / x ] ph <-> A. x ( x = y -> ph ) )
5	1 3	equsal	|- ( A. x ( x = y -> ph ) <-> ps )
6	4 5	bitri	|- ( [ y / x ] ph <-> ps )