Description: Define the property of a wff ph that the setvar variables x and y are interchangeable. For an alternate definition using implicit substitution and a temporary setvar variable see ichcircshi . Another, equivalent definition using two temporary setvar variables is provided in dfich2 . (Contributed by AV, 29-Jul-2023)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | df-ich | ⊢ ( [ 𝑥 ⇄ 𝑦 ] 𝜑 ↔ ∀ 𝑥 ∀ 𝑦 ( [ 𝑥 / 𝑎 ] [ 𝑦 / 𝑥 ] [ 𝑎 / 𝑦 ] 𝜑 ↔ 𝜑 ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 0 | vx | ⊢ 𝑥 | |
| 1 | vy | ⊢ 𝑦 | |
| 2 | wph | ⊢ 𝜑 | |
| 3 | 2 0 1 | wich | ⊢ [ 𝑥 ⇄ 𝑦 ] 𝜑 |
| 4 | va | ⊢ 𝑎 | |
| 5 | 2 1 4 | wsb | ⊢ [ 𝑎 / 𝑦 ] 𝜑 |
| 6 | 5 0 1 | wsb | ⊢ [ 𝑦 / 𝑥 ] [ 𝑎 / 𝑦 ] 𝜑 |
| 7 | 6 4 0 | wsb | ⊢ [ 𝑥 / 𝑎 ] [ 𝑦 / 𝑥 ] [ 𝑎 / 𝑦 ] 𝜑 |
| 8 | 7 2 | wb | ⊢ ( [ 𝑥 / 𝑎 ] [ 𝑦 / 𝑥 ] [ 𝑎 / 𝑦 ] 𝜑 ↔ 𝜑 ) |
| 9 | 8 1 | wal | ⊢ ∀ 𝑦 ( [ 𝑥 / 𝑎 ] [ 𝑦 / 𝑥 ] [ 𝑎 / 𝑦 ] 𝜑 ↔ 𝜑 ) |
| 10 | 9 0 | wal | ⊢ ∀ 𝑥 ∀ 𝑦 ( [ 𝑥 / 𝑎 ] [ 𝑦 / 𝑥 ] [ 𝑎 / 𝑦 ] 𝜑 ↔ 𝜑 ) |
| 11 | 3 10 | wb | ⊢ ( [ 𝑥 ⇄ 𝑦 ] 𝜑 ↔ ∀ 𝑥 ∀ 𝑦 ( [ 𝑥 / 𝑎 ] [ 𝑦 / 𝑥 ] [ 𝑎 / 𝑦 ] 𝜑 ↔ 𝜑 ) ) |