Step | Hyp | Ref
| Expression |
1 | | sbccow 3704 |
. 2
⊢
([𝐴 / 𝑧][𝑧 / 𝑥]∀𝑦 ∈ 𝐵 𝜑 ↔ [𝐴 / 𝑥]∀𝑦 ∈ 𝐵 𝜑) |
2 | | simpl 486 |
. . 3
⊢ ((𝐴 ∈ 𝑉 ∧ Ⅎ𝑦𝐴) → 𝐴 ∈ 𝑉) |
3 | | sbsbc 3685 |
. . . . 5
⊢ ([𝑧 / 𝑥]∀𝑦 ∈ 𝐵 𝜑 ↔ [𝑧 / 𝑥]∀𝑦 ∈ 𝐵 𝜑) |
4 | | nfcv 2900 |
. . . . . . 7
⊢
Ⅎ𝑥𝐵 |
5 | | nfs1v 2161 |
. . . . . . 7
⊢
Ⅎ𝑥[𝑧 / 𝑥]𝜑 |
6 | 4, 5 | nfralw 3139 |
. . . . . 6
⊢
Ⅎ𝑥∀𝑦 ∈ 𝐵 [𝑧 / 𝑥]𝜑 |
7 | | sbequ12 2253 |
. . . . . . 7
⊢ (𝑥 = 𝑧 → (𝜑 ↔ [𝑧 / 𝑥]𝜑)) |
8 | 7 | ralbidv 3110 |
. . . . . 6
⊢ (𝑥 = 𝑧 → (∀𝑦 ∈ 𝐵 𝜑 ↔ ∀𝑦 ∈ 𝐵 [𝑧 / 𝑥]𝜑)) |
9 | 6, 8 | sbiev 2317 |
. . . . 5
⊢ ([𝑧 / 𝑥]∀𝑦 ∈ 𝐵 𝜑 ↔ ∀𝑦 ∈ 𝐵 [𝑧 / 𝑥]𝜑) |
10 | 3, 9 | bitr3i 280 |
. . . 4
⊢
([𝑧 / 𝑥]∀𝑦 ∈ 𝐵 𝜑 ↔ ∀𝑦 ∈ 𝐵 [𝑧 / 𝑥]𝜑) |
11 | | nfnfc1 2903 |
. . . . . . 7
⊢
Ⅎ𝑦Ⅎ𝑦𝐴 |
12 | | nfcvd 2901 |
. . . . . . . 8
⊢
(Ⅎ𝑦𝐴 → Ⅎ𝑦𝑧) |
13 | | id 22 |
. . . . . . . 8
⊢
(Ⅎ𝑦𝐴 → Ⅎ𝑦𝐴) |
14 | 12, 13 | nfeqd 2910 |
. . . . . . 7
⊢
(Ⅎ𝑦𝐴 → Ⅎ𝑦 𝑧 = 𝐴) |
15 | 11, 14 | nfan1 2202 |
. . . . . 6
⊢
Ⅎ𝑦(Ⅎ𝑦𝐴 ∧ 𝑧 = 𝐴) |
16 | | dfsbcq2 3684 |
. . . . . . 7
⊢ (𝑧 = 𝐴 → ([𝑧 / 𝑥]𝜑 ↔ [𝐴 / 𝑥]𝜑)) |
17 | 16 | adantl 485 |
. . . . . 6
⊢
((Ⅎ𝑦𝐴 ∧ 𝑧 = 𝐴) → ([𝑧 / 𝑥]𝜑 ↔ [𝐴 / 𝑥]𝜑)) |
18 | 15, 17 | ralbid 3146 |
. . . . 5
⊢
((Ⅎ𝑦𝐴 ∧ 𝑧 = 𝐴) → (∀𝑦 ∈ 𝐵 [𝑧 / 𝑥]𝜑 ↔ ∀𝑦 ∈ 𝐵 [𝐴 / 𝑥]𝜑)) |
19 | 18 | adantll 714 |
. . . 4
⊢ (((𝐴 ∈ 𝑉 ∧ Ⅎ𝑦𝐴) ∧ 𝑧 = 𝐴) → (∀𝑦 ∈ 𝐵 [𝑧 / 𝑥]𝜑 ↔ ∀𝑦 ∈ 𝐵 [𝐴 / 𝑥]𝜑)) |
20 | 10, 19 | syl5bb 286 |
. . 3
⊢ (((𝐴 ∈ 𝑉 ∧ Ⅎ𝑦𝐴) ∧ 𝑧 = 𝐴) → ([𝑧 / 𝑥]∀𝑦 ∈ 𝐵 𝜑 ↔ ∀𝑦 ∈ 𝐵 [𝐴 / 𝑥]𝜑)) |
21 | 2, 20 | sbcied 3725 |
. 2
⊢ ((𝐴 ∈ 𝑉 ∧ Ⅎ𝑦𝐴) → ([𝐴 / 𝑧][𝑧 / 𝑥]∀𝑦 ∈ 𝐵 𝜑 ↔ ∀𝑦 ∈ 𝐵 [𝐴 / 𝑥]𝜑)) |
22 | 1, 21 | bitr3id 288 |
1
⊢ ((𝐴 ∈ 𝑉 ∧ Ⅎ𝑦𝐴) → ([𝐴 / 𝑥]∀𝑦 ∈ 𝐵 𝜑 ↔ ∀𝑦 ∈ 𝐵 [𝐴 / 𝑥]𝜑)) |