Theorem bj-equsexvwd

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

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

Proof

Step	Hyp	Ref	Expression
1		bj-equsexvwd.nf0	|- ( ph -> A. x ph )
2		bj-equsexvwd.nf	|- ( ph -> F// x ch )
3		bj-equsexvwd.is	|- ( ( ph /\ x = y ) -> ( ps <-> ch ) )
4		alinexa	|- ( A. x ( x = y -> -. ps ) <-> -. E. x ( x = y /\ ps ) )
5		bj-nnfnt	|- ( F// x ch <-> F// x -. ch )
6	2 5	sylib	|- ( ph -> F// x -. ch )
7	3	notbid	|- ( ( ph /\ x = y ) -> ( -. ps <-> -. ch ) )
8	1 6 7	bj-equsalvwd	|- ( ph -> ( A. x ( x = y -> -. ps ) <-> -. ch ) )
9	4 8	bitr3id	|- ( ph -> ( -. E. x ( x = y /\ ps ) <-> -. ch ) )
10	9	con4bid	|- ( ph -> ( E. x ( x = y /\ ps ) <-> ch ) )