This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 dfsb ⊢ ( [ 𝑡 / 𝑥 ] ¬ 𝜑 ↔ ∀ 𝑦 ( 𝑦 = 𝑡 → ∀ 𝑥 ( 𝑥 = 𝑦 → ¬ 𝜑 ) ) )
2 alinexa ⊢ ( ∀ 𝑥 ( 𝑥 = 𝑦 → ¬ 𝜑 ) ↔ ¬ ∃ 𝑥 ( 𝑥 = 𝑦 ∧ 𝜑 ) )
3 2 imbi2i ⊢ ( ( 𝑦 = 𝑡 → ∀ 𝑥 ( 𝑥 = 𝑦 → ¬ 𝜑 ) ) ↔ ( 𝑦 = 𝑡 → ¬ ∃ 𝑥 ( 𝑥 = 𝑦 ∧ 𝜑 ) ) )
4 3 albii ⊢ ( ∀ 𝑦 ( 𝑦 = 𝑡 → ∀ 𝑥 ( 𝑥 = 𝑦 → ¬ 𝜑 ) ) ↔ ∀ 𝑦 ( 𝑦 = 𝑡 → ¬ ∃ 𝑥 ( 𝑥 = 𝑦 ∧ 𝜑 ) ) )
5 alinexa ⊢ ( ∀ 𝑦 ( 𝑦 = 𝑡 → ¬ ∃ 𝑥 ( 𝑥 = 𝑦 ∧ 𝜑 ) ) ↔ ¬ ∃ 𝑦 ( 𝑦 = 𝑡 ∧ ∃ 𝑥 ( 𝑥 = 𝑦 ∧ 𝜑 ) ) )
6 dfsb7 ⊢ ( [ 𝑡 / 𝑥 ] 𝜑 ↔ ∃ 𝑦 ( 𝑦 = 𝑡 ∧ ∃ 𝑥 ( 𝑥 = 𝑦 ∧ 𝜑 ) ) )
7 5 6 xchbinxr ⊢ ( ∀ 𝑦 ( 𝑦 = 𝑡 → ¬ ∃ 𝑥 ( 𝑥 = 𝑦 ∧ 𝜑 ) ) ↔ ¬ [ 𝑡 / 𝑥 ] 𝜑 )
8 1 4 7 3bitri ⊢ ( [ 𝑡 / 𝑥 ] ¬ 𝜑 ↔ ¬ [ 𝑡 / 𝑥 ] 𝜑 )