Theorem wl-equsald

Description: Deduction version of equsal . (Contributed by Wolf Lammen, 27-Jul-2019)

	Ref	Expression
Hypotheses	wl-equsald.1	|- F/ x ph
	wl-equsald.2	|- ( ph -> F/ x ch )
	wl-equsald.3	|- ( ph -> ( x = y -> ( ps <-> ch ) ) )
Assertion	wl-equsald	|- ( ph -> ( A. x ( x = y -> ps ) <-> ch ) )

Proof

Step	Hyp	Ref	Expression
1		wl-equsald.1	|- F/ x ph
2		wl-equsald.2	|- ( ph -> F/ x ch )
3		wl-equsald.3	|- ( ph -> ( x = y -> ( ps <-> ch ) ) )
4		19.23t	|- ( F/ x ch -> ( A. x ( x = y -> ch ) <-> ( E. x x = y -> ch ) ) )
5	2 4	syl	|- ( ph -> ( A. x ( x = y -> ch ) <-> ( E. x x = y -> ch ) ) )
6	3	pm5.74d	|- ( ph -> ( ( x = y -> ps ) <-> ( x = y -> ch ) ) )
7	1 6	albid	|- ( ph -> ( A. x ( x = y -> ps ) <-> A. x ( x = y -> ch ) ) )
8		ax6e	|- E. x x = y
9	8	a1bi	|- ( ch <-> ( E. x x = y -> ch ) )
10	9	a1i	|- ( ph -> ( ch <-> ( E. x x = y -> ch ) ) )
11	5 7 10	3bitr4d	|- ( ph -> ( A. x ( x = y -> ps ) <-> ch ) )