Description: A theorem is interchangeable. (Contributed by SN, 4-May-2024)
Ref | Expression | ||
---|---|---|---|
Hypothesis | icht.1 | ⊢ 𝜑 | |
Assertion | icht | ⊢ [ 𝑥 ⇄ 𝑦 ] 𝜑 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | icht.1 | ⊢ 𝜑 | |
2 | 1 | sbt | ⊢ [ 𝑎 / 𝑦 ] 𝜑 |
3 | 2 | sbt | ⊢ [ 𝑦 / 𝑥 ] [ 𝑎 / 𝑦 ] 𝜑 |
4 | 3 | sbt | ⊢ [ 𝑥 / 𝑎 ] [ 𝑦 / 𝑥 ] [ 𝑎 / 𝑦 ] 𝜑 |
5 | 4 1 | 2th | ⊢ ( [ 𝑥 / 𝑎 ] [ 𝑦 / 𝑥 ] [ 𝑎 / 𝑦 ] 𝜑 ↔ 𝜑 ) |
6 | 5 | gen2 | ⊢ ∀ 𝑥 ∀ 𝑦 ( [ 𝑥 / 𝑎 ] [ 𝑦 / 𝑥 ] [ 𝑎 / 𝑦 ] 𝜑 ↔ 𝜑 ) |
7 | df-ich | ⊢ ( [ 𝑥 ⇄ 𝑦 ] 𝜑 ↔ ∀ 𝑥 ∀ 𝑦 ( [ 𝑥 / 𝑎 ] [ 𝑦 / 𝑥 ] [ 𝑎 / 𝑦 ] 𝜑 ↔ 𝜑 ) ) | |
8 | 6 7 | mpbir | ⊢ [ 𝑥 ⇄ 𝑦 ] 𝜑 |