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	|- F/ x ps
	wl-equsal.2	|- ( x = y -> ( ph <-> ps ) )
Assertion	wl-equsal	|- ( A. x ( x = y -> ph ) <-> ps )

Proof

Step	Hyp	Ref	Expression
1		wl-equsal.1	|- F/ x ps
2		wl-equsal.2	|- ( x = y -> ( ph <-> ps ) )
3		nftru	|- F/ x T.
4	1	a1i	|- ( T. -> F/ x ps )
5	2	a1i	|- ( T. -> ( x = y -> ( ph <-> ps ) ) )
6	3 4 5	wl-equsald	|- ( T. -> ( A. x ( x = y -> ph ) <-> ps ) )
7	6	mptru	|- ( A. x ( x = y -> ph ) <-> ps )