Theorem wl-equsal1t

Description: The expression x = y in antecedent position plays an important role in predicate logic, namely in implicit substitution. However, occasionally it is irrelevant, and can safely be dropped. A sufficient condition for this is when x (or y or both) is not free in ph .

This theorem is more fundamental than equsal , spimt or sbft , to which it is related. (Contributed by Wolf Lammen, 19-Aug-2018)

	Ref	Expression
Assertion	wl-equsal1t	⊢ ( Ⅎ 𝑥 𝜑 → ( ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) ↔ 𝜑 ) )

Proof

Step	Hyp	Ref	Expression
1		nfnf1	⊢ Ⅎ 𝑥 Ⅎ 𝑥 𝜑
2		id	⊢ ( Ⅎ 𝑥 𝜑 → Ⅎ 𝑥 𝜑 )
3		biid	⊢ ( 𝜑 ↔ 𝜑 )
4	3	2a1i	⊢ ( Ⅎ 𝑥 𝜑 → ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜑 ) ) )
5	1 2 4	wl-equsald	⊢ ( Ⅎ 𝑥 𝜑 → ( ∀ 𝑥 ( 𝑥 = 𝑦 → 𝜑 ) ↔ 𝜑 ) )