Theorem pm13.196a 44988

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 2291	. 2 ⊢ (¬ 𝜑 ↔ ∃𝑦(𝑦 = 𝑥 ∧ [𝑦 / 𝑥] ¬ 𝜑))
2		sbalex 2280	. 2 ⊢ (∃𝑦(𝑦 = 𝑥 ∧ [𝑦 / 𝑥] ¬ 𝜑) ↔ ∀𝑦(𝑦 = 𝑥 → [𝑦 / 𝑥] ¬ 𝜑))
3		sbn 2317	. . . . 5 ⊢ ([𝑦 / 𝑥] ¬ 𝜑 ↔ ¬ [𝑦 / 𝑥]𝜑)
4	3	imbi2i 339	. . . 4 ⊢ ((𝑦 = 𝑥 → [𝑦 / 𝑥] ¬ 𝜑) ↔ (𝑦 = 𝑥 → ¬ [𝑦 / 𝑥]𝜑))
5		con2b 362	. . . 4 ⊢ ((𝑦 = 𝑥 → ¬ [𝑦 / 𝑥]𝜑) ↔ ([𝑦 / 𝑥]𝜑 → ¬ 𝑦 = 𝑥))
6		df-ne 2961	. . . . . 6 ⊢ (𝑦 ≠ 𝑥 ↔ ¬ 𝑦 = 𝑥)
7	6	bicomi 227	. . . . 5 ⊢ (¬ 𝑦 = 𝑥 ↔ 𝑦 ≠ 𝑥)
8	7	imbi2i 339	. . . 4 ⊢ (([𝑦 / 𝑥]𝜑 → ¬ 𝑦 = 𝑥) ↔ ([𝑦 / 𝑥]𝜑 → 𝑦 ≠ 𝑥))
9	4, 5, 8	3bitri 300	. . 3 ⊢ ((𝑦 = 𝑥 → [𝑦 / 𝑥] ¬ 𝜑) ↔ ([𝑦 / 𝑥]𝜑 → 𝑦 ≠ 𝑥))
10	9	albii 1842	. 2 ⊢ (∀𝑦(𝑦 = 𝑥 → [𝑦 / 𝑥] ¬ 𝜑) ↔ ∀𝑦([𝑦 / 𝑥]𝜑 → 𝑦 ≠ 𝑥))
11	1, 2, 10	3bitri 300	1 ⊢ (¬ 𝜑 ↔ ∀𝑦([𝑦 / 𝑥]𝜑 → 𝑦 ≠ 𝑥))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 400  ∀wal 1561  ∃wex 1802  [wsb 2093   ≠ wne 2960

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-10 2178  ax-12 2215

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1803  df-nf 1807  df-sb 2094  df-ne 2961

This theorem is referenced by: (None)