Step | Hyp | Ref
| Expression |
1 | | sbccow 3739 |
. 2
⊢
([𝐴 / 𝑧][𝑧 / 𝑥]∀𝑦 ∈ 𝐵 𝜑 ↔ [𝐴 / 𝑥]∀𝑦 ∈ 𝐵 𝜑) |
2 | | simpl 483 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ Ⅎ𝑦𝐴) → 𝐴 ∈ 𝑉) |
3 | | sbsbc 3720 |
. . . . 5
⊢ ([𝑧 / 𝑥]∀𝑦 ∈ 𝐵 𝜑 ↔ [𝑧 / 𝑥]∀𝑦 ∈ 𝐵 𝜑) |
4 | | nfcv 2907 |
. . . . . . 7
⊢
Ⅎ𝑥𝐵 |
5 | | nfs1v 2153 |
. . . . . . 7
⊢
Ⅎ𝑥[𝑧 / 𝑥]𝜑 |
6 | 4, 5 | nfralw 3151 |
. . . . . 6
⊢
Ⅎ𝑥∀𝑦 ∈ 𝐵 [𝑧 / 𝑥]𝜑 |
7 | | sbequ12 2244 |
. . . . . . 7
⊢ (𝑥 = 𝑧 → (𝜑 ↔ [𝑧 / 𝑥]𝜑)) |
8 | 7 | ralbidv 3112 |
. . . . . 6
⊢ (𝑥 = 𝑧 → (∀𝑦 ∈ 𝐵 𝜑 ↔ ∀𝑦 ∈ 𝐵 [𝑧 / 𝑥]𝜑)) |
9 | 6, 8 | sbiev 2309 |
. . . . 5
⊢ ([𝑧 / 𝑥]∀𝑦 ∈ 𝐵 𝜑 ↔ ∀𝑦 ∈ 𝐵 [𝑧 / 𝑥]𝜑) |
10 | 3, 9 | bitr3i 276 |
. . . 4
⊢
([𝑧 / 𝑥]∀𝑦 ∈ 𝐵 𝜑 ↔ ∀𝑦 ∈ 𝐵 [𝑧 / 𝑥]𝜑) |
11 | | nfnfc1 2910 |
. . . . . . 7
⊢
Ⅎ𝑦Ⅎ𝑦𝐴 |
12 | | nfcvd 2908 |
. . . . . . . 8
⊢
(Ⅎ𝑦𝐴 → Ⅎ𝑦𝑧) |
13 | | id 22 |
. . . . . . . 8
⊢
(Ⅎ𝑦𝐴 → Ⅎ𝑦𝐴) |
14 | 12, 13 | nfeqd 2917 |
. . . . . . 7
⊢
(Ⅎ𝑦𝐴 → Ⅎ𝑦 𝑧 = 𝐴) |
15 | 11, 14 | nfan1 2193 |
. . . . . 6
⊢
Ⅎ𝑦(Ⅎ𝑦𝐴 ∧ 𝑧 = 𝐴) |
16 | | dfsbcq2 3719 |
. . . . . . 7
⊢ (𝑧 = 𝐴 → ([𝑧 / 𝑥]𝜑 ↔ [𝐴 / 𝑥]𝜑)) |
17 | 16 | adantl 482 |
. . . . . 6
⊢
((Ⅎ𝑦𝐴 ∧ 𝑧 = 𝐴) → ([𝑧 / 𝑥]𝜑 ↔ [𝐴 / 𝑥]𝜑)) |
18 | 15, 17 | ralbid 3161 |
. . . . 5
⊢
((Ⅎ𝑦𝐴 ∧ 𝑧 = 𝐴) → (∀𝑦 ∈ 𝐵 [𝑧 / 𝑥]𝜑 ↔ ∀𝑦 ∈ 𝐵 [𝐴 / 𝑥]𝜑)) |
19 | 18 | adantll 711 |
. . . 4
⊢ (((𝐴 ∈ 𝑉 ∧ Ⅎ𝑦𝐴) ∧ 𝑧 = 𝐴) → (∀𝑦 ∈ 𝐵 [𝑧 / 𝑥]𝜑 ↔ ∀𝑦 ∈ 𝐵 [𝐴 / 𝑥]𝜑)) |
20 | 10, 19 | bitrid 282 |
. . 3
⊢ (((𝐴 ∈ 𝑉 ∧ Ⅎ𝑦𝐴) ∧ 𝑧 = 𝐴) → ([𝑧 / 𝑥]∀𝑦 ∈ 𝐵 𝜑 ↔ ∀𝑦 ∈ 𝐵 [𝐴 / 𝑥]𝜑)) |
21 | 2, 20 | sbcied 3761 |
. 2
⊢ ((𝐴 ∈ 𝑉 ∧ Ⅎ𝑦𝐴) → ([𝐴 / 𝑧][𝑧 / 𝑥]∀𝑦 ∈ 𝐵 𝜑 ↔ ∀𝑦 ∈ 𝐵 [𝐴 / 𝑥]𝜑)) |
22 | 1, 21 | bitr3id 285 |
1
⊢ ((𝐴 ∈ 𝑉 ∧ Ⅎ𝑦𝐴) → ([𝐴 / 𝑥]∀𝑦 ∈ 𝐵 𝜑 ↔ ∀𝑦 ∈ 𝐵 [𝐴 / 𝑥]𝜑)) |