Theorem wl-equsaldv

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

	Ref	Expression
Hypotheses	wl-equsald.1	$$⊢Ⅎx\phi$$
	wl-equsald.2	$$⊢\phi \to Ⅎx\chi$$
	wl-equsald.3	$$⊢\phi \to \left(x=y\to \left(\psi \leftrightarrow \chi \right)\right)$$
Assertion	wl-equsaldv	$$⊢\phi \to \left(\forall x\left(x=y\to \psi \right)\leftrightarrow \chi \right)$$

Proof

Step	Hyp	Ref	Expression
1		wl-equsald.1	$$⊢Ⅎx\phi$$
2		wl-equsald.2	$$⊢\phi \to Ⅎx\chi$$
3		wl-equsald.3	$$⊢\phi \to \left(x=y\to \left(\psi \leftrightarrow \chi \right)\right)$$
4		19.23t	$$⊢Ⅎx\chi \to \left(\forall x\left(x=y\to \chi \right)\leftrightarrow \left(\exists xx=y\to \chi \right)\right)$$
5	2 4	syl	$$⊢\phi \to \left(\forall x\left(x=y\to \chi \right)\leftrightarrow \left(\exists xx=y\to \chi \right)\right)$$
6	3	pm5.74d	$$⊢\phi \to \left(\left(x=y\to \psi \right)\leftrightarrow \left(x=y\to \chi \right)\right)$$
7	1 6	albid	$$⊢\phi \to \left(\forall x\left(x=y\to \psi \right)\leftrightarrow \forall x\left(x=y\to \chi \right)\right)$$
8		ax6ev	$$⊢\exists xx=y$$
9	8	a1bi	$$⊢\chi \leftrightarrow \left(\exists xx=y\to \chi \right)$$
10	9	a1i	$$⊢\phi \to \left(\chi \leftrightarrow \left(\exists xx=y\to \chi \right)\right)$$
11	5 7 10	3bitr4d	$$⊢\phi \to \left(\forall x\left(x=y\to \psi \right)\leftrightarrow \chi \right)$$