Step |
Hyp |
Ref |
Expression |
1 |
|
ichf.1 |
⊢ Ⅎ 𝑥 𝜑 |
2 |
|
ichf.2 |
⊢ Ⅎ 𝑦 𝜑 |
3 |
2
|
sbf |
⊢ ( [ 𝑎 / 𝑦 ] 𝜑 ↔ 𝜑 ) |
4 |
3
|
sbbii |
⊢ ( [ 𝑦 / 𝑥 ] [ 𝑎 / 𝑦 ] 𝜑 ↔ [ 𝑦 / 𝑥 ] 𝜑 ) |
5 |
1
|
sbf |
⊢ ( [ 𝑦 / 𝑥 ] 𝜑 ↔ 𝜑 ) |
6 |
4 5
|
bitri |
⊢ ( [ 𝑦 / 𝑥 ] [ 𝑎 / 𝑦 ] 𝜑 ↔ 𝜑 ) |
7 |
6
|
sbbii |
⊢ ( [ 𝑥 / 𝑎 ] [ 𝑦 / 𝑥 ] [ 𝑎 / 𝑦 ] 𝜑 ↔ [ 𝑥 / 𝑎 ] 𝜑 ) |
8 |
|
sbv |
⊢ ( [ 𝑥 / 𝑎 ] 𝜑 ↔ 𝜑 ) |
9 |
7 8
|
bitri |
⊢ ( [ 𝑥 / 𝑎 ] [ 𝑦 / 𝑥 ] [ 𝑎 / 𝑦 ] 𝜑 ↔ 𝜑 ) |
10 |
9
|
gen2 |
⊢ ∀ 𝑥 ∀ 𝑦 ( [ 𝑥 / 𝑎 ] [ 𝑦 / 𝑥 ] [ 𝑎 / 𝑦 ] 𝜑 ↔ 𝜑 ) |
11 |
|
df-ich |
⊢ ( [ 𝑥 ⇄ 𝑦 ] 𝜑 ↔ ∀ 𝑥 ∀ 𝑦 ( [ 𝑥 / 𝑎 ] [ 𝑦 / 𝑥 ] [ 𝑎 / 𝑦 ] 𝜑 ↔ 𝜑 ) ) |
12 |
10 11
|
mpbir |
⊢ [ 𝑥 ⇄ 𝑦 ] 𝜑 |