Theorem wl-sbid2ft

Description: A more general version of sbid2vw . (Contributed by Wolf Lammen, 14-May-2019)

	Ref	Expression
Assertion	wl-sbid2ft	|- ( F/ x ph -> ( [ y / x ] [ x / y ] ph <-> ph ) )

Proof

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