Step | Hyp | Ref
| Expression |
1 | | dfsbcq 3774 |
. . . . 5
⊢ (𝑧 = 𝐴 → ([𝑧 / 𝑥][𝐵 / 𝑦]𝜑 ↔ [𝐴 / 𝑥][𝐵 / 𝑦]𝜑)) |
2 | | csbeq1 3886 |
. . . . . 6
⊢ (𝑧 = 𝐴 → ⦋𝑧 / 𝑥⦌𝐵 = ⦋𝐴 / 𝑥⦌𝐵) |
3 | 2 | sbceq1d 3777 |
. . . . 5
⊢ (𝑧 = 𝐴 → ([⦋𝑧 / 𝑥⦌𝐵 / 𝑦]𝜑 ↔ [⦋𝐴 / 𝑥⦌𝐵 / 𝑦]𝜑)) |
4 | 1, 3 | bibi12d 348 |
. . . 4
⊢ (𝑧 = 𝐴 → (([𝑧 / 𝑥][𝐵 / 𝑦]𝜑 ↔ [⦋𝑧 / 𝑥⦌𝐵 / 𝑦]𝜑) ↔ ([𝐴 / 𝑥][𝐵 / 𝑦]𝜑 ↔ [⦋𝐴 / 𝑥⦌𝐵 / 𝑦]𝜑))) |
5 | 4 | imbi2d 343 |
. . 3
⊢ (𝑧 = 𝐴 → ((∀𝑦Ⅎ𝑥𝜑 → ([𝑧 / 𝑥][𝐵 / 𝑦]𝜑 ↔ [⦋𝑧 / 𝑥⦌𝐵 / 𝑦]𝜑)) ↔ (∀𝑦Ⅎ𝑥𝜑 → ([𝐴 / 𝑥][𝐵 / 𝑦]𝜑 ↔ [⦋𝐴 / 𝑥⦌𝐵 / 𝑦]𝜑)))) |
6 | | vex 3497 |
. . . . 5
⊢ 𝑧 ∈ V |
7 | 6 | a1i 11 |
. . . 4
⊢
(∀𝑦Ⅎ𝑥𝜑 → 𝑧 ∈ V) |
8 | | csbeq1a 3897 |
. . . . . 6
⊢ (𝑥 = 𝑧 → 𝐵 = ⦋𝑧 / 𝑥⦌𝐵) |
9 | 8 | sbceq1d 3777 |
. . . . 5
⊢ (𝑥 = 𝑧 → ([𝐵 / 𝑦]𝜑 ↔ [⦋𝑧 / 𝑥⦌𝐵 / 𝑦]𝜑)) |
10 | 9 | adantl 484 |
. . . 4
⊢
((∀𝑦Ⅎ𝑥𝜑 ∧ 𝑥 = 𝑧) → ([𝐵 / 𝑦]𝜑 ↔ [⦋𝑧 / 𝑥⦌𝐵 / 𝑦]𝜑)) |
11 | | nfnf1 2158 |
. . . . 5
⊢
Ⅎ𝑥Ⅎ𝑥𝜑 |
12 | 11 | nfal 2342 |
. . . 4
⊢
Ⅎ𝑥∀𝑦Ⅎ𝑥𝜑 |
13 | | nfa1 2155 |
. . . . 5
⊢
Ⅎ𝑦∀𝑦Ⅎ𝑥𝜑 |
14 | | nfcsb1v 3907 |
. . . . . 6
⊢
Ⅎ𝑥⦋𝑧 / 𝑥⦌𝐵 |
15 | 14 | a1i 11 |
. . . . 5
⊢
(∀𝑦Ⅎ𝑥𝜑 → Ⅎ𝑥⦋𝑧 / 𝑥⦌𝐵) |
16 | | sp 2182 |
. . . . 5
⊢
(∀𝑦Ⅎ𝑥𝜑 → Ⅎ𝑥𝜑) |
17 | 13, 15, 16 | nfsbcdw 3793 |
. . . 4
⊢
(∀𝑦Ⅎ𝑥𝜑 → Ⅎ𝑥[⦋𝑧 / 𝑥⦌𝐵 / 𝑦]𝜑) |
18 | 7, 10, 12, 17 | sbciedf 3813 |
. . 3
⊢
(∀𝑦Ⅎ𝑥𝜑 → ([𝑧 / 𝑥][𝐵 / 𝑦]𝜑 ↔ [⦋𝑧 / 𝑥⦌𝐵 / 𝑦]𝜑)) |
19 | 5, 18 | vtoclg 3567 |
. 2
⊢ (𝐴 ∈ 𝑉 → (∀𝑦Ⅎ𝑥𝜑 → ([𝐴 / 𝑥][𝐵 / 𝑦]𝜑 ↔ [⦋𝐴 / 𝑥⦌𝐵 / 𝑦]𝜑))) |
20 | 19 | imp 409 |
1
⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑦Ⅎ𝑥𝜑) → ([𝐴 / 𝑥][𝐵 / 𝑦]𝜑 ↔ [⦋𝐴 / 𝑥⦌𝐵 / 𝑦]𝜑)) |