Theorem sbn

Description: Negation inside and outside of substitution are equivalent. (Contributed by NM, 14-May-1993) (Proof shortened by Wolf Lammen, 30-Apr-2018) Revise df-sb . (Revised by BJ, 25-Dec-2020)

	Ref	Expression
Assertion	sbn	⊢ ( [ 𝑡 / 𝑥 ] ¬ 𝜑 ↔ ¬ [ 𝑡 / 𝑥 ] 𝜑 )

Proof

Step	Hyp	Ref	Expression
1		df-sb	⊢ ( [ 𝑡 / 𝑥 ] ¬ 𝜑 ↔ ∀ 𝑦 ( 𝑦 = 𝑡 → ∀ 𝑥 ( 𝑥 = 𝑦 → ¬ 𝜑 ) ) )
2		alinexa	⊢ ( ∀ 𝑥 ( 𝑥 = 𝑦 → ¬ 𝜑 ) ↔ ¬ ∃ 𝑥 ( 𝑥 = 𝑦 ∧ 𝜑 ) )
3	2	imbi2i	⊢ ( ( 𝑦 = 𝑡 → ∀ 𝑥 ( 𝑥 = 𝑦 → ¬ 𝜑 ) ) ↔ ( 𝑦 = 𝑡 → ¬ ∃ 𝑥 ( 𝑥 = 𝑦 ∧ 𝜑 ) ) )
4	3	albii	⊢ ( ∀ 𝑦 ( 𝑦 = 𝑡 → ∀ 𝑥 ( 𝑥 = 𝑦 → ¬ 𝜑 ) ) ↔ ∀ 𝑦 ( 𝑦 = 𝑡 → ¬ ∃ 𝑥 ( 𝑥 = 𝑦 ∧ 𝜑 ) ) )
5		alinexa	⊢ ( ∀ 𝑦 ( 𝑦 = 𝑡 → ¬ ∃ 𝑥 ( 𝑥 = 𝑦 ∧ 𝜑 ) ) ↔ ¬ ∃ 𝑦 ( 𝑦 = 𝑡 ∧ ∃ 𝑥 ( 𝑥 = 𝑦 ∧ 𝜑 ) ) )
6		dfsb7	⊢ ( [ 𝑡 / 𝑥 ] 𝜑 ↔ ∃ 𝑦 ( 𝑦 = 𝑡 ∧ ∃ 𝑥 ( 𝑥 = 𝑦 ∧ 𝜑 ) ) )
7	5 6	xchbinxr	⊢ ( ∀ 𝑦 ( 𝑦 = 𝑡 → ¬ ∃ 𝑥 ( 𝑥 = 𝑦 ∧ 𝜑 ) ) ↔ ¬ [ 𝑡 / 𝑥 ] 𝜑 )
8	1 4 7	3bitri	⊢ ( [ 𝑡 / 𝑥 ] ¬ 𝜑 ↔ ¬ [ 𝑡 / 𝑥 ] 𝜑 )