Theorem wl-nfsbtv

Description: Closed form of nfsbv . (Contributed by Wolf Lammen, 2-May-2025)

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

Proof

Step	Hyp	Ref	Expression
1		stdpc4	|- ( A. x F/ z ph -> [ y / x ] F/ z ph )
2		sbnf	|- ( [ y / x ] F/ z ph <-> F/ z [ y / x ] ph )
3	1 2	sylib	|- ( A. x F/ z ph -> F/ z [ y / x ] ph )