Description: A setvar variable is always interchangeable with itself. (Contributed by AV, 29-Jul-2023)
Ref | Expression | ||
---|---|---|---|
Assertion | ichid | ⊢ [ 𝑥 ⇄ 𝑥 ] 𝜑 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sbid | ⊢ ( [ 𝑥 / 𝑥 ] [ 𝑎 / 𝑥 ] 𝜑 ↔ [ 𝑎 / 𝑥 ] 𝜑 ) | |
2 | 1 | sbbii | ⊢ ( [ 𝑥 / 𝑎 ] [ 𝑥 / 𝑥 ] [ 𝑎 / 𝑥 ] 𝜑 ↔ [ 𝑥 / 𝑎 ] [ 𝑎 / 𝑥 ] 𝜑 ) |
3 | sbid2vw | ⊢ ( [ 𝑥 / 𝑎 ] [ 𝑎 / 𝑥 ] 𝜑 ↔ 𝜑 ) | |
4 | 2 3 | bitri | ⊢ ( [ 𝑥 / 𝑎 ] [ 𝑥 / 𝑥 ] [ 𝑎 / 𝑥 ] 𝜑 ↔ 𝜑 ) |
5 | 4 | gen2 | ⊢ ∀ 𝑥 ∀ 𝑥 ( [ 𝑥 / 𝑎 ] [ 𝑥 / 𝑥 ] [ 𝑎 / 𝑥 ] 𝜑 ↔ 𝜑 ) |
6 | df-ich | ⊢ ( [ 𝑥 ⇄ 𝑥 ] 𝜑 ↔ ∀ 𝑥 ∀ 𝑥 ( [ 𝑥 / 𝑎 ] [ 𝑥 / 𝑥 ] [ 𝑎 / 𝑥 ] 𝜑 ↔ 𝜑 ) ) | |
7 | 5 6 | mpbir | ⊢ [ 𝑥 ⇄ 𝑥 ] 𝜑 |