Step |
Hyp |
Ref |
Expression |
1 |
|
sbequ12 |
⊢ ( 𝑦 = 𝑧 → ( ∀ 𝑥 𝜑 ↔ [ 𝑧 / 𝑦 ] ∀ 𝑥 𝜑 ) ) |
2 |
1
|
sps |
⊢ ( ∀ 𝑦 𝑦 = 𝑧 → ( ∀ 𝑥 𝜑 ↔ [ 𝑧 / 𝑦 ] ∀ 𝑥 𝜑 ) ) |
3 |
|
sbequ12 |
⊢ ( 𝑦 = 𝑧 → ( 𝜑 ↔ [ 𝑧 / 𝑦 ] 𝜑 ) ) |
4 |
3
|
sps |
⊢ ( ∀ 𝑦 𝑦 = 𝑧 → ( 𝜑 ↔ [ 𝑧 / 𝑦 ] 𝜑 ) ) |
5 |
4
|
dral2 |
⊢ ( ∀ 𝑦 𝑦 = 𝑧 → ( ∀ 𝑥 𝜑 ↔ ∀ 𝑥 [ 𝑧 / 𝑦 ] 𝜑 ) ) |
6 |
2 5
|
bitr3d |
⊢ ( ∀ 𝑦 𝑦 = 𝑧 → ( [ 𝑧 / 𝑦 ] ∀ 𝑥 𝜑 ↔ ∀ 𝑥 [ 𝑧 / 𝑦 ] 𝜑 ) ) |
7 |
6
|
adantl |
⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ ∀ 𝑦 𝑦 = 𝑧 ) → ( [ 𝑧 / 𝑦 ] ∀ 𝑥 𝜑 ↔ ∀ 𝑥 [ 𝑧 / 𝑦 ] 𝜑 ) ) |
8 |
|
sb4b |
⊢ ( ¬ ∀ 𝑦 𝑦 = 𝑧 → ( [ 𝑧 / 𝑦 ] ∀ 𝑥 𝜑 ↔ ∀ 𝑦 ( 𝑦 = 𝑧 → ∀ 𝑥 𝜑 ) ) ) |
9 |
8
|
adantl |
⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ ¬ ∀ 𝑦 𝑦 = 𝑧 ) → ( [ 𝑧 / 𝑦 ] ∀ 𝑥 𝜑 ↔ ∀ 𝑦 ( 𝑦 = 𝑧 → ∀ 𝑥 𝜑 ) ) ) |
10 |
|
nfnae |
⊢ Ⅎ 𝑥 ¬ ∀ 𝑦 𝑦 = 𝑧 |
11 |
|
sb4b |
⊢ ( ¬ ∀ 𝑦 𝑦 = 𝑧 → ( [ 𝑧 / 𝑦 ] 𝜑 ↔ ∀ 𝑦 ( 𝑦 = 𝑧 → 𝜑 ) ) ) |
12 |
10 11
|
albid |
⊢ ( ¬ ∀ 𝑦 𝑦 = 𝑧 → ( ∀ 𝑥 [ 𝑧 / 𝑦 ] 𝜑 ↔ ∀ 𝑥 ∀ 𝑦 ( 𝑦 = 𝑧 → 𝜑 ) ) ) |
13 |
|
alcom |
⊢ ( ∀ 𝑥 ∀ 𝑦 ( 𝑦 = 𝑧 → 𝜑 ) ↔ ∀ 𝑦 ∀ 𝑥 ( 𝑦 = 𝑧 → 𝜑 ) ) |
14 |
12 13
|
bitrdi |
⊢ ( ¬ ∀ 𝑦 𝑦 = 𝑧 → ( ∀ 𝑥 [ 𝑧 / 𝑦 ] 𝜑 ↔ ∀ 𝑦 ∀ 𝑥 ( 𝑦 = 𝑧 → 𝜑 ) ) ) |
15 |
|
nfnae |
⊢ Ⅎ 𝑦 ¬ ∀ 𝑥 𝑥 = 𝑦 |
16 |
|
nfeqf1 |
⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → Ⅎ 𝑥 𝑦 = 𝑧 ) |
17 |
|
19.21t |
⊢ ( Ⅎ 𝑥 𝑦 = 𝑧 → ( ∀ 𝑥 ( 𝑦 = 𝑧 → 𝜑 ) ↔ ( 𝑦 = 𝑧 → ∀ 𝑥 𝜑 ) ) ) |
18 |
16 17
|
syl |
⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ( ∀ 𝑥 ( 𝑦 = 𝑧 → 𝜑 ) ↔ ( 𝑦 = 𝑧 → ∀ 𝑥 𝜑 ) ) ) |
19 |
15 18
|
albid |
⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ( ∀ 𝑦 ∀ 𝑥 ( 𝑦 = 𝑧 → 𝜑 ) ↔ ∀ 𝑦 ( 𝑦 = 𝑧 → ∀ 𝑥 𝜑 ) ) ) |
20 |
14 19
|
sylan9bbr |
⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ ¬ ∀ 𝑦 𝑦 = 𝑧 ) → ( ∀ 𝑥 [ 𝑧 / 𝑦 ] 𝜑 ↔ ∀ 𝑦 ( 𝑦 = 𝑧 → ∀ 𝑥 𝜑 ) ) ) |
21 |
9 20
|
bitr4d |
⊢ ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∧ ¬ ∀ 𝑦 𝑦 = 𝑧 ) → ( [ 𝑧 / 𝑦 ] ∀ 𝑥 𝜑 ↔ ∀ 𝑥 [ 𝑧 / 𝑦 ] 𝜑 ) ) |
22 |
7 21
|
pm2.61dan |
⊢ ( ¬ ∀ 𝑥 𝑥 = 𝑦 → ( [ 𝑧 / 𝑦 ] ∀ 𝑥 𝜑 ↔ ∀ 𝑥 [ 𝑧 / 𝑦 ] 𝜑 ) ) |