Description: Setvar variables are interchangeable in a wff they do not appear in. (Contributed by SN, 23-Nov-2023)
Ref | Expression | ||
---|---|---|---|
Assertion | ichv | ⊢ [ 𝑥 ⇄ 𝑦 ] 𝜑 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sbv | ⊢ ( [ 𝑎 / 𝑦 ] 𝜑 ↔ 𝜑 ) | |
2 | 1 | sbbii | ⊢ ( [ 𝑦 / 𝑥 ] [ 𝑎 / 𝑦 ] 𝜑 ↔ [ 𝑦 / 𝑥 ] 𝜑 ) |
3 | sbv | ⊢ ( [ 𝑦 / 𝑥 ] 𝜑 ↔ 𝜑 ) | |
4 | 2 3 | bitri | ⊢ ( [ 𝑦 / 𝑥 ] [ 𝑎 / 𝑦 ] 𝜑 ↔ 𝜑 ) |
5 | 4 | sbbii | ⊢ ( [ 𝑥 / 𝑎 ] [ 𝑦 / 𝑥 ] [ 𝑎 / 𝑦 ] 𝜑 ↔ [ 𝑥 / 𝑎 ] 𝜑 ) |
6 | sbv | ⊢ ( [ 𝑥 / 𝑎 ] 𝜑 ↔ 𝜑 ) | |
7 | 5 6 | bitri | ⊢ ( [ 𝑥 / 𝑎 ] [ 𝑦 / 𝑥 ] [ 𝑎 / 𝑦 ] 𝜑 ↔ 𝜑 ) |
8 | 7 | gen2 | ⊢ ∀ 𝑥 ∀ 𝑦 ( [ 𝑥 / 𝑎 ] [ 𝑦 / 𝑥 ] [ 𝑎 / 𝑦 ] 𝜑 ↔ 𝜑 ) |
9 | df-ich | ⊢ ( [ 𝑥 ⇄ 𝑦 ] 𝜑 ↔ ∀ 𝑥 ∀ 𝑦 ( [ 𝑥 / 𝑎 ] [ 𝑦 / 𝑥 ] [ 𝑎 / 𝑦 ] 𝜑 ↔ 𝜑 ) ) | |
10 | 8 9 | mpbir | ⊢ [ 𝑥 ⇄ 𝑦 ] 𝜑 |