Theorem sbn 2317

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 2100. (Revised by BJ, 25-Dec-2020.)

Assertion

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

Proof of Theorem sbn

Dummy variable 𝑦 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		dfsb 2101	. 2 ⊢ ([𝑡 / 𝑥] ¬ 𝜑 ↔ ∀𝑦(𝑦 = 𝑡 → ∀𝑥(𝑥 = 𝑦 → ¬ 𝜑)))
2		alinexa 1876	. . . 4 ⊢ (∀𝑥(𝑥 = 𝑦 → ¬ 𝜑) ↔ ¬ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑))
3	2	imbi2i 339	. . 3 ⊢ ((𝑦 = 𝑡 → ∀𝑥(𝑥 = 𝑦 → ¬ 𝜑)) ↔ (𝑦 = 𝑡 → ¬ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑)))
4	3	albii 1852	. 2 ⊢ (∀𝑦(𝑦 = 𝑡 → ∀𝑥(𝑥 = 𝑦 → ¬ 𝜑)) ↔ ∀𝑦(𝑦 = 𝑡 → ¬ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑)))
5		alinexa 1876	. . 3 ⊢ (∀𝑦(𝑦 = 𝑡 → ¬ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑)) ↔ ¬ ∃𝑦(𝑦 = 𝑡 ∧ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑)))
6		dfsb7 2316	. . 3 ⊢ ([𝑡 / 𝑥]𝜑 ↔ ∃𝑦(𝑦 = 𝑡 ∧ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑)))
7	5, 6	xchbinxr 338	. 2 ⊢ (∀𝑦(𝑦 = 𝑡 → ¬ ∃𝑥(𝑥 = 𝑦 ∧ 𝜑)) ↔ ¬ [𝑡 / 𝑥]𝜑)
8	1, 4, 7	3bitri 300	1 ⊢ ([𝑡 / 𝑥] ¬ 𝜑 ↔ ¬ [𝑡 / 𝑥]𝜑)

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 401  ∀wal 1568  ∃wex 1812  [wsb 2099

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-10 2179  ax-12 2216

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-nf 1817  df-sb 2100

This theorem is used by:  sbex  2318  sbi2  2339  sbor  2343  sbcng  3793  difab  4263  difopab  5819  wl-sb8eft  38265  wl-sb8et  38267  pm13.196a  45184  ichn  48265