Theorem wl-sb8t

Description: Substitution of variable in universal quantifier. Closed form of sb8 . (Contributed by Wolf Lammen, 27-Jul-2019)

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

Proof

Step	Hyp	Ref	Expression
1		nfa1	|- F/ x A. x F/ y ph
2		nfnf1	|- F/ y F/ y ph
3	2	nfal	|- F/ y A. x F/ y ph
4		sp	|- ( A. x F/ y ph -> F/ y ph )
5		wl-nfs1t	|- ( F/ y ph -> F/ x [ y / x ] ph )
6	5	sps	|- ( A. x F/ y ph -> F/ x [ y / x ] ph )
7		sbequ12	|- ( x = y -> ( ph <-> [ y / x ] ph ) )
8	7	a1i	|- ( A. x F/ y ph -> ( x = y -> ( ph <-> [ y / x ] ph ) ) )
9	1 3 4 6 8	cbv2	|- ( A. x F/ y ph -> ( A. x ph <-> A. y [ y / x ] ph ) )