Theorem wl-equsal

Description: A useful equivalence related to substitution. (Contributed by NM, 2-Jun-1993) (Proof shortened by Andrew Salmon, 12-Aug-2011) (Revised by Mario Carneiro, 3-Oct-2016) It seems proving wl-equsald first, and then deriving more specialized versions wl-equsal and wl-equsal1t then is more efficient than the other way round, which is possible, too. See also equsal . (Revised by Wolf Lammen, 27-Jul-2019) (Proof modification is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		wl-equsal.1	⊢ Ⅎ 𝑥 𝜓
2		wl-equsal.2	⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜓 ) )
3		nftru	⊢ Ⅎ 𝑥 ⊤
4	1	a1i	⊢ ( ⊤ → Ⅎ 𝑥 𝜓 )
5	2	a1i	⊢ ( ⊤ → ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜓 ) ) )
6	3 4 5	wl-equsald	⊢ ( ⊤ → ( ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) ↔ 𝜓 ) )
7	6	mptru	⊢ ( ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) ↔ 𝜓 )