Theorem nsb

Description: Generalization rule for negated wff. (Contributed by Steven Nguyen, 3-May-2023)

	Ref	Expression
Hypothesis	nsb.1	⊢ ¬ 𝜑
Assertion	nsb	⊢ ¬ [ 𝑥 / 𝑦 ] 𝜑

Proof

Step	Hyp	Ref	Expression
1		nsb.1	⊢ ¬ 𝜑
2	1	nex	⊢ ¬ ∃ 𝑦 𝜑
3		spsbe	⊢ ( [ 𝑥 / 𝑦 ] 𝜑 → ∃ 𝑦 𝜑 )
4	2 3	mto	⊢ ¬ [ 𝑥 / 𝑦 ] 𝜑