Theorem wl-nfsbtv

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

	Ref	Expression
Assertion	wl-nfsbtv	⊢ ( ∀ 𝑥 Ⅎ 𝑧 𝜑 → Ⅎ 𝑧 [ 𝑦 / 𝑥 ] 𝜑 )

Proof

Step	Hyp	Ref	Expression
1		stdpc4	⊢ ( ∀ 𝑥 Ⅎ 𝑧 𝜑 → [ 𝑦 / 𝑥 ] Ⅎ 𝑧 𝜑 )
2		sbnf	⊢ ( [ 𝑦 / 𝑥 ] Ⅎ 𝑧 𝜑 ↔ Ⅎ 𝑧 [ 𝑦 / 𝑥 ] 𝜑 )
3	1 2	sylib	⊢ ( ∀ 𝑥 Ⅎ 𝑧 𝜑 → Ⅎ 𝑧 [ 𝑦 / 𝑥 ] 𝜑 )