Theorem wl-nfsbtv

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

	Ref	Expression
Assertion	wl-nfsbtv	$$⊢\forall xℲz\phi \to Ⅎz\left[y/x\right]\phi$$

Proof

Step	Hyp	Ref	Expression
1		stdpc4	$$⊢\forall xℲz\phi \to \left[y/x\right]Ⅎz\phi$$
2		sbnf	$$⊢\left[y/x\right]Ⅎz\phi \leftrightarrow Ⅎz\left[y/x\right]\phi$$
3	1 2	sylib	$$⊢\forall xℲz\phi \to Ⅎz\left[y/x\right]\phi$$