Theorem wl-sb6rft

Description: A specialization of wl-equsal1t . Closed form of sb6rf . (Contributed by Wolf Lammen, 27-Jul-2019)

	Ref	Expression
Assertion	wl-sb6rft	|- ( F/ x ph -> ( ph <-> A. x ( x = y -> [ x / y ] ph ) ) )

Proof

Step	Hyp	Ref	Expression
1		nfnf1	|- F/ x F/ x ph
2		id	|- ( F/ x ph -> F/ x ph )
3		sbequ12r	|- ( x = y -> ( [ x / y ] ph <-> ph ) )
4	3	a1i	|- ( F/ x ph -> ( x = y -> ( [ x / y ] ph <-> ph ) ) )
5	1 2 4	wl-equsald	|- ( F/ x ph -> ( A. x ( x = y -> [ x / y ] ph ) <-> ph ) )
6	5	bicomd	|- ( F/ x ph -> ( ph <-> A. x ( x = y -> [ x / y ] ph ) ) )