Step |
Hyp |
Ref |
Expression |
1 |
|
drsb1 |
⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ( [ 𝑧 / 𝑥 ] [ 𝑦 / 𝑥 ] 𝜑 ↔ [ 𝑧 / 𝑦 ] [ 𝑦 / 𝑥 ] 𝜑 ) ) |
2 |
|
nfae |
⊢ Ⅎ 𝑥 ∀ 𝑥 𝑥 = 𝑦 |
3 |
|
sbequ12a |
⊢ ( 𝑥 = 𝑦 → ( [ 𝑦 / 𝑥 ] 𝜑 ↔ [ 𝑥 / 𝑦 ] 𝜑 ) ) |
4 |
3
|
sps |
⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ( [ 𝑦 / 𝑥 ] 𝜑 ↔ [ 𝑥 / 𝑦 ] 𝜑 ) ) |
5 |
2 4
|
sbbid |
⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ( [ 𝑧 / 𝑥 ] [ 𝑦 / 𝑥 ] 𝜑 ↔ [ 𝑧 / 𝑥 ] [ 𝑥 / 𝑦 ] 𝜑 ) ) |
6 |
1 5
|
bitr3d |
⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ( [ 𝑧 / 𝑦 ] [ 𝑦 / 𝑥 ] 𝜑 ↔ [ 𝑧 / 𝑥 ] [ 𝑥 / 𝑦 ] 𝜑 ) ) |
7 |
|
nfnae |
⊢ Ⅎ 𝑦 ¬ ∀ 𝑥 𝑥 = 𝑦 |
8 |
|
nfnae |
⊢ Ⅎ 𝑥 ¬ ∀ 𝑥 𝑥 = 𝑦 |
9 |
|
nfsb2 |
⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → Ⅎ 𝑥 [ 𝑦 / 𝑥 ] 𝜑 ) |
10 |
7 8 9
|
sbco2d |
⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ( [ 𝑧 / 𝑥 ] [ 𝑥 / 𝑦 ] [ 𝑦 / 𝑥 ] 𝜑 ↔ [ 𝑧 / 𝑦 ] [ 𝑦 / 𝑥 ] 𝜑 ) ) |
11 |
|
sbco |
⊢ ( [ 𝑥 / 𝑦 ] [ 𝑦 / 𝑥 ] 𝜑 ↔ [ 𝑥 / 𝑦 ] 𝜑 ) |
12 |
11
|
sbbii |
⊢ ( [ 𝑧 / 𝑥 ] [ 𝑥 / 𝑦 ] [ 𝑦 / 𝑥 ] 𝜑 ↔ [ 𝑧 / 𝑥 ] [ 𝑥 / 𝑦 ] 𝜑 ) |
13 |
10 12
|
bitr3di |
⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ( [ 𝑧 / 𝑦 ] [ 𝑦 / 𝑥 ] 𝜑 ↔ [ 𝑧 / 𝑥 ] [ 𝑥 / 𝑦 ] 𝜑 ) ) |
14 |
6 13
|
pm2.61i |
⊢ ( [ 𝑧 / 𝑦 ] [ 𝑦 / 𝑥 ] 𝜑 ↔ [ 𝑧 / 𝑥 ] [ 𝑥 / 𝑦 ] 𝜑 ) |