Theorem wl-equsald

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

	Ref	Expression
Hypotheses	wl-equsald.1	⊢ Ⅎ 𝑥 𝜑
	wl-equsald.2	⊢ ( 𝜑 → Ⅎ 𝑥 𝜒 )
	wl-equsald.3	⊢ ( 𝜑 → ( 𝑥 = 𝑦 → ( 𝜓 ↔ 𝜒 ) ) )
Assertion	wl-equsald	⊢ ( 𝜑 → ( ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜓 ) ↔ 𝜒 ) )

Proof

Step	Hyp	Ref	Expression
1		wl-equsald.1	⊢ Ⅎ 𝑥 𝜑
2		wl-equsald.2	⊢ ( 𝜑 → Ⅎ 𝑥 𝜒 )
3		wl-equsald.3	⊢ ( 𝜑 → ( 𝑥 = 𝑦 → ( 𝜓 ↔ 𝜒 ) ) )
4		19.23t	⊢ ( Ⅎ 𝑥 𝜒 → ( ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜒 ) ↔ ( ∃ 𝑥 𝑥 = 𝑦 → 𝜒 ) ) )
5	2 4	syl	⊢ ( 𝜑 → ( ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜒 ) ↔ ( ∃ 𝑥 𝑥 = 𝑦 → 𝜒 ) ) )
6	3	pm5.74d	⊢ ( 𝜑 → ( ( 𝑥 = 𝑦 → 𝜓 ) ↔ ( 𝑥 = 𝑦 → 𝜒 ) ) )
7	1 6	albid	⊢ ( 𝜑 → ( ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜓 ) ↔ ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜒 ) ) )
8		ax6e	⊢ ∃ 𝑥 𝑥 = 𝑦
9	8	a1bi	⊢ ( 𝜒 ↔ ( ∃ 𝑥 𝑥 = 𝑦 → 𝜒 ) )
10	9	a1i	⊢ ( 𝜑 → ( 𝜒 ↔ ( ∃ 𝑥 𝑥 = 𝑦 → 𝜒 ) ) )
11	5 7 10	3bitr4d	⊢ ( 𝜑 → ( ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜓 ) ↔ 𝜒 ) )