Step |
Hyp |
Ref |
Expression |
1 |
|
sb8v |
⊢ ( ∀ 𝑥 ( 𝑥 ∈ 𝐴 → 𝜑 ) ↔ ∀ 𝑦 [ 𝑦 / 𝑥 ] ( 𝑥 ∈ 𝐴 → 𝜑 ) ) |
2 |
|
df-ral |
⊢ ( ∀ 𝑥 ∈ 𝐴 𝜑 ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐴 → 𝜑 ) ) |
3 |
|
df-ral |
⊢ ( ∀ 𝑦 ∈ 𝐴 [ 𝑦 / 𝑥 ] 𝜑 ↔ ∀ 𝑦 ( 𝑦 ∈ 𝐴 → [ 𝑦 / 𝑥 ] 𝜑 ) ) |
4 |
|
eleq1w |
⊢ ( 𝑥 = 𝑦 → ( 𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴 ) ) |
5 |
4
|
imbi1d |
⊢ ( 𝑥 = 𝑦 → ( ( 𝑥 ∈ 𝐴 → 𝜑 ) ↔ ( 𝑦 ∈ 𝐴 → 𝜑 ) ) ) |
6 |
5
|
pm5.74i |
⊢ ( ( 𝑥 = 𝑦 → ( 𝑥 ∈ 𝐴 → 𝜑 ) ) ↔ ( 𝑥 = 𝑦 → ( 𝑦 ∈ 𝐴 → 𝜑 ) ) ) |
7 |
6
|
albii |
⊢ ( ∀ 𝑥 ( 𝑥 = 𝑦 → ( 𝑥 ∈ 𝐴 → 𝜑 ) ) ↔ ∀ 𝑥 ( 𝑥 = 𝑦 → ( 𝑦 ∈ 𝐴 → 𝜑 ) ) ) |
8 |
|
sb6 |
⊢ ( [ 𝑦 / 𝑥 ] ( 𝑥 ∈ 𝐴 → 𝜑 ) ↔ ∀ 𝑥 ( 𝑥 = 𝑦 → ( 𝑥 ∈ 𝐴 → 𝜑 ) ) ) |
9 |
|
sb6 |
⊢ ( [ 𝑦 / 𝑥 ] ( 𝑦 ∈ 𝐴 → 𝜑 ) ↔ ∀ 𝑥 ( 𝑥 = 𝑦 → ( 𝑦 ∈ 𝐴 → 𝜑 ) ) ) |
10 |
7 8 9
|
3bitr4i |
⊢ ( [ 𝑦 / 𝑥 ] ( 𝑥 ∈ 𝐴 → 𝜑 ) ↔ [ 𝑦 / 𝑥 ] ( 𝑦 ∈ 𝐴 → 𝜑 ) ) |
11 |
|
sbrimvw |
⊢ ( [ 𝑦 / 𝑥 ] ( 𝑦 ∈ 𝐴 → 𝜑 ) ↔ ( 𝑦 ∈ 𝐴 → [ 𝑦 / 𝑥 ] 𝜑 ) ) |
12 |
10 11
|
bitr2i |
⊢ ( ( 𝑦 ∈ 𝐴 → [ 𝑦 / 𝑥 ] 𝜑 ) ↔ [ 𝑦 / 𝑥 ] ( 𝑥 ∈ 𝐴 → 𝜑 ) ) |
13 |
12
|
albii |
⊢ ( ∀ 𝑦 ( 𝑦 ∈ 𝐴 → [ 𝑦 / 𝑥 ] 𝜑 ) ↔ ∀ 𝑦 [ 𝑦 / 𝑥 ] ( 𝑥 ∈ 𝐴 → 𝜑 ) ) |
14 |
3 13
|
bitri |
⊢ ( ∀ 𝑦 ∈ 𝐴 [ 𝑦 / 𝑥 ] 𝜑 ↔ ∀ 𝑦 [ 𝑦 / 𝑥 ] ( 𝑥 ∈ 𝐴 → 𝜑 ) ) |
15 |
1 2 14
|
3bitr4i |
⊢ ( ∀ 𝑥 ∈ 𝐴 𝜑 ↔ ∀ 𝑦 ∈ 𝐴 [ 𝑦 / 𝑥 ] 𝜑 ) |