Theorem pm13.196a 42032

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 2246	. 2 ⊢ (¬ 𝜑 ↔ ∃𝑦(𝑦 = 𝑥 ∧ [𝑦 / 𝑥] ¬ 𝜑))
2		sbalex 2235	. 2 ⊢ (∃𝑦(𝑦 = 𝑥 ∧ [𝑦 / 𝑥] ¬ 𝜑) ↔ ∀𝑦(𝑦 = 𝑥 → [𝑦 / 𝑥] ¬ 𝜑))
3		sbn 2277	. . . . 5 ⊢ ([𝑦 / 𝑥] ¬ 𝜑 ↔ ¬ [𝑦 / 𝑥]𝜑)
4	3	imbi2i 336	. . . 4 ⊢ ((𝑦 = 𝑥 → [𝑦 / 𝑥] ¬ 𝜑) ↔ (𝑦 = 𝑥 → ¬ [𝑦 / 𝑥]𝜑))
5		con2b 360	. . . 4 ⊢ ((𝑦 = 𝑥 → ¬ [𝑦 / 𝑥]𝜑) ↔ ([𝑦 / 𝑥]𝜑 → ¬ 𝑦 = 𝑥))
6		df-ne 2944	. . . . . 6 ⊢ (𝑦 ≠ 𝑥 ↔ ¬ 𝑦 = 𝑥)
7	6	bicomi 223	. . . . 5 ⊢ (¬ 𝑦 = 𝑥 ↔ 𝑦 ≠ 𝑥)
8	7	imbi2i 336	. . . 4 ⊢ (([𝑦 / 𝑥]𝜑 → ¬ 𝑦 = 𝑥) ↔ ([𝑦 / 𝑥]𝜑 → 𝑦 ≠ 𝑥))
9	4, 5, 8	3bitri 297	. . 3 ⊢ ((𝑦 = 𝑥 → [𝑦 / 𝑥] ¬ 𝜑) ↔ ([𝑦 / 𝑥]𝜑 → 𝑦 ≠ 𝑥))
10	9	albii 1822	. 2 ⊢ (∀𝑦(𝑦 = 𝑥 → [𝑦 / 𝑥] ¬ 𝜑) ↔ ∀𝑦([𝑦 / 𝑥]𝜑 → 𝑦 ≠ 𝑥))
11	1, 2, 10	3bitri 297	1 ⊢ (¬ 𝜑 ↔ ∀𝑦([𝑦 / 𝑥]𝜑 → 𝑦 ≠ 𝑥))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 396  ∀wal 1537  ∃wex 1782  [wsb 2067   ≠ wne 2943

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-10 2137  ax-12 2171

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-ex 1783  df-nf 1787  df-sb 2068  df-ne 2944

This theorem is referenced by: (None)