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	$$⊢Ⅎx\psi$$
	wl-equsal.2	$$⊢x=y\to \left(\phi \leftrightarrow \psi \right)$$
Assertion	wl-equsal	$$⊢\forall x\left(x=y\to \phi \right)\leftrightarrow \psi$$

Proof

Step	Hyp	Ref	Expression
1		wl-equsal.1	$$⊢Ⅎx\psi$$
2		wl-equsal.2	$$⊢x=y\to \left(\phi \leftrightarrow \psi \right)$$
3		nftru	$$⊢Ⅎx\top$$
4	1	a1i	$$⊢\top \to Ⅎx\psi$$
5	2	a1i	$$⊢\top \to \left(x=y\to \left(\phi \leftrightarrow \psi \right)\right)$$
6	3 4 5	wl-equsald	$$⊢\top \to \left(\forall x\left(x=y\to \phi \right)\leftrightarrow \psi \right)$$
7	6	mptru	$$⊢\forall x\left(x=y\to \phi \right)\leftrightarrow \psi$$