Theorem pm13.196a 41921

Description: Theorem *13.196 in [WhiteheadRussell] p. 179. The only difference is the position of the substituted variable. (Contributed by Andrew Salmon, 3-Jun-2011.)

Assertion

Ref	Expression
pm13.196a	⊢ (¬ 𝜑 ↔ ∀𝑦([𝑦 / 𝑥]𝜑 → 𝑦 ≠ 𝑥))

Distinct variable groups:   𝑥,𝑦   𝜑,𝑦

Allowed substitution hint:   𝜑(𝑥)

Proof of Theorem pm13.196a

Step	Hyp	Ref	Expression
1		sbelx 2249	. 2 ⊢ (¬ 𝜑 ↔ ∃𝑦(𝑦 = 𝑥 ∧ [𝑦 / 𝑥] ¬ 𝜑))
2		sbalex 2238	. 2 ⊢ (∃𝑦(𝑦 = 𝑥 ∧ [𝑦 / 𝑥] ¬ 𝜑) ↔ ∀𝑦(𝑦 = 𝑥 → [𝑦 / 𝑥] ¬ 𝜑))
3		sbn 2280	. . . . 5 ⊢ ([𝑦 / 𝑥] ¬ 𝜑 ↔ ¬ [𝑦 / 𝑥]𝜑)
4	3	imbi2i 335	. . . 4 ⊢ ((𝑦 = 𝑥 → [𝑦 / 𝑥] ¬ 𝜑) ↔ (𝑦 = 𝑥 → ¬ [𝑦 / 𝑥]𝜑))
5		con2b 359	. . . 4 ⊢ ((𝑦 = 𝑥 → ¬ [𝑦 / 𝑥]𝜑) ↔ ([𝑦 / 𝑥]𝜑 → ¬ 𝑦 = 𝑥))
6		df-ne 2943	. . . . . 6 ⊢ (𝑦 ≠ 𝑥 ↔ ¬ 𝑦 = 𝑥)
7	6	bicomi 223	. . . . 5 ⊢ (¬ 𝑦 = 𝑥 ↔ 𝑦 ≠ 𝑥)
8	7	imbi2i 335	. . . 4 ⊢ (([𝑦 / 𝑥]𝜑 → ¬ 𝑦 = 𝑥) ↔ ([𝑦 / 𝑥]𝜑 → 𝑦 ≠ 𝑥))
9	4, 5, 8	3bitri 296	. . 3 ⊢ ((𝑦 = 𝑥 → [𝑦 / 𝑥] ¬ 𝜑) ↔ ([𝑦 / 𝑥]𝜑 → 𝑦 ≠ 𝑥))
10	9	albii 1823	. 2 ⊢ (∀𝑦(𝑦 = 𝑥 → [𝑦 / 𝑥] ¬ 𝜑) ↔ ∀𝑦([𝑦 / 𝑥]𝜑 → 𝑦 ≠ 𝑥))
11	1, 2, 10	3bitri 296	1 ⊢ (¬ 𝜑 ↔ ∀𝑦([𝑦 / 𝑥]𝜑 → 𝑦 ≠ 𝑥))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 395  ∀wal 1537  ∃wex 1783  [wsb 2068   ≠ wne 2942

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-10 2139  ax-12 2173

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-ex 1784  df-nf 1788  df-sb 2069  df-ne 2943

This theorem is referenced by: (None)