Theorem bj-equsalvwd

Description: Variant of equsalvw . (Contributed by BJ, 7-Oct-2024)

	Ref	Expression
Hypotheses	bj-equsalvwd.nf0	|- ( ph -> A. x ph )
	bj-equsalvwd.nf	|- ( ph -> F// x ch )
	bj-equsalvwd.is	|- ( ( ph /\ x = y ) -> ( ps <-> ch ) )
Assertion	bj-equsalvwd	|- ( ph -> ( A. x ( x = y -> ps ) <-> ch ) )

Proof

Step	Hyp	Ref	Expression
1		bj-equsalvwd.nf0	|- ( ph -> A. x ph )
2		bj-equsalvwd.nf	|- ( ph -> F// x ch )
3		bj-equsalvwd.is	|- ( ( ph /\ x = y ) -> ( ps <-> ch ) )
4	3	pm5.74da	|- ( ph -> ( ( x = y -> ps ) <-> ( x = y -> ch ) ) )
5	1 4	albidh	|- ( ph -> ( A. x ( x = y -> ps ) <-> A. x ( x = y -> ch ) ) )
6		bj-equsvt	|- ( F// x ch -> ( A. x ( x = y -> ch ) <-> ch ) )
7	2 6	syl	|- ( ph -> ( A. x ( x = y -> ch ) <-> ch ) )
8	5 7	bitrd	|- ( ph -> ( A. x ( x = y -> ps ) <-> ch ) )