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	$$⊢Ⅎx\phi \to \left(\forall x\left(x=y\to \phi \right)\leftrightarrow \phi \right)$$

Proof

Step	Hyp	Ref	Expression
1		nfnf1	$$⊢ℲxℲx\phi$$
2		id	$$⊢Ⅎx\phi \to Ⅎx\phi$$
3		biid	$$⊢\phi \leftrightarrow \phi$$
4	3	2a1i	$$⊢Ⅎx\phi \to \left(x=y\to \left(\phi \leftrightarrow \phi \right)\right)$$
5	1 2 4	wl-equsald	$$⊢Ⅎx\phi \to \left(\forall x\left(x=y\to \phi \right)\leftrightarrow \phi \right)$$