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

Metamath Proof Explorer

Theorem pm13.196a

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)

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

Proof

Step Hyp Ref Expression
1 sbelx ⊢ ( ¬ 𝜑 ↔ ∃ 𝑦 ( 𝑦 = 𝑥 ∧ [ 𝑦 / 𝑥 ] ¬ 𝜑 ) )
2 sbalex ⊢ ( ∃ 𝑦 ( 𝑦 = 𝑥 ∧ [ 𝑦 / 𝑥 ] ¬ 𝜑 ) ↔ ∀ 𝑦 ( 𝑦 = 𝑥 → [ 𝑦 / 𝑥 ] ¬ 𝜑 ) )
3 sbn ⊢ ( [ 𝑦 / 𝑥 ] ¬ 𝜑 ↔ ¬ [ 𝑦 / 𝑥 ] 𝜑 )
4 3 imbi2i ⊢ ( ( 𝑦 = 𝑥 → [ 𝑦 / 𝑥 ] ¬ 𝜑 ) ↔ ( 𝑦 = 𝑥 → ¬ [ 𝑦 / 𝑥 ] 𝜑 ) )
5 con2b ⊢ ( ( 𝑦 = 𝑥 → ¬ [ 𝑦 / 𝑥 ] 𝜑 ) ↔ ( [ 𝑦 / 𝑥 ] 𝜑 → ¬ 𝑦 = 𝑥 ) )
6 df-ne ⊢ ( 𝑦 ≠ 𝑥 ↔ ¬ 𝑦 = 𝑥 )
7 6 bicomi ⊢ ( ¬ 𝑦 = 𝑥 ↔ 𝑦 ≠ 𝑥 )
8 7 imbi2i ⊢ ( ( [ 𝑦 / 𝑥 ] 𝜑 → ¬ 𝑦 = 𝑥 ) ↔ ( [ 𝑦 / 𝑥 ] 𝜑 → 𝑦 ≠ 𝑥 ) )
9 4 5 8 3bitri ⊢ ( ( 𝑦 = 𝑥 → [ 𝑦 / 𝑥 ] ¬ 𝜑 ) ↔ ( [ 𝑦 / 𝑥 ] 𝜑 → 𝑦 ≠ 𝑥 ) )
10 9 albii ⊢ ( ∀ 𝑦 ( 𝑦 = 𝑥 → [ 𝑦 / 𝑥 ] ¬ 𝜑 ) ↔ ∀ 𝑦 ( [ 𝑦 / 𝑥 ] 𝜑 → 𝑦 ≠ 𝑥 ) )
11 1 2 10 3bitri ⊢ ( ¬ 𝜑 ↔ ∀ 𝑦 ( [ 𝑦 / 𝑥 ] 𝜑 → 𝑦 ≠ 𝑥 ) )