Step | Hyp | Ref
| Expression |
1 | | dfsbcq 3723 |
. . . . 5
⊢ (𝑧 = 𝐴 → ([𝑧 / 𝑥][𝐵 / 𝑦]𝜑 ↔ [𝐴 / 𝑥][𝐵 / 𝑦]𝜑)) |
2 | | csbeq1 3840 |
. . . . . 6
⊢ (𝑧 = 𝐴 → ⦋𝑧 / 𝑥⦌𝐵 = ⦋𝐴 / 𝑥⦌𝐵) |
3 | 2 | sbceq1d 3726 |
. . . . 5
⊢ (𝑧 = 𝐴 → ([⦋𝑧 / 𝑥⦌𝐵 / 𝑦]𝜑 ↔ [⦋𝐴 / 𝑥⦌𝐵 / 𝑦]𝜑)) |
4 | 1, 3 | bibi12d 346 |
. . . 4
⊢ (𝑧 = 𝐴 → (([𝑧 / 𝑥][𝐵 / 𝑦]𝜑 ↔ [⦋𝑧 / 𝑥⦌𝐵 / 𝑦]𝜑) ↔ ([𝐴 / 𝑥][𝐵 / 𝑦]𝜑 ↔ [⦋𝐴 / 𝑥⦌𝐵 / 𝑦]𝜑))) |
5 | 4 | imbi2d 341 |
. . 3
⊢ (𝑧 = 𝐴 → ((∀𝑦Ⅎ𝑥𝜑 → ([𝑧 / 𝑥][𝐵 / 𝑦]𝜑 ↔ [⦋𝑧 / 𝑥⦌𝐵 / 𝑦]𝜑)) ↔ (∀𝑦Ⅎ𝑥𝜑 → ([𝐴 / 𝑥][𝐵 / 𝑦]𝜑 ↔ [⦋𝐴 / 𝑥⦌𝐵 / 𝑦]𝜑)))) |
6 | | vex 3441 |
. . . . 5
⊢ 𝑧 ∈ V |
7 | 6 | a1i 11 |
. . . 4
⊢
(∀𝑦Ⅎ𝑥𝜑 → 𝑧 ∈ V) |
8 | | csbeq1a 3851 |
. . . . . 6
⊢ (𝑥 = 𝑧 → 𝐵 = ⦋𝑧 / 𝑥⦌𝐵) |
9 | 8 | sbceq1d 3726 |
. . . . 5
⊢ (𝑥 = 𝑧 → ([𝐵 / 𝑦]𝜑 ↔ [⦋𝑧 / 𝑥⦌𝐵 / 𝑦]𝜑)) |
10 | 9 | adantl 483 |
. . . 4
⊢
((∀𝑦Ⅎ𝑥𝜑 ∧ 𝑥 = 𝑧) → ([𝐵 / 𝑦]𝜑 ↔ [⦋𝑧 / 𝑥⦌𝐵 / 𝑦]𝜑)) |
11 | | nfnf1 2149 |
. . . . 5
⊢
Ⅎ𝑥Ⅎ𝑥𝜑 |
12 | 11 | nfal 2315 |
. . . 4
⊢
Ⅎ𝑥∀𝑦Ⅎ𝑥𝜑 |
13 | | nfa1 2146 |
. . . . 5
⊢
Ⅎ𝑦∀𝑦Ⅎ𝑥𝜑 |
14 | | nfcsb1v 3862 |
. . . . . 6
⊢
Ⅎ𝑥⦋𝑧 / 𝑥⦌𝐵 |
15 | 14 | a1i 11 |
. . . . 5
⊢
(∀𝑦Ⅎ𝑥𝜑 → Ⅎ𝑥⦋𝑧 / 𝑥⦌𝐵) |
16 | | sp 2174 |
. . . . 5
⊢
(∀𝑦Ⅎ𝑥𝜑 → Ⅎ𝑥𝜑) |
17 | 13, 15, 16 | nfsbcdw 3742 |
. . . 4
⊢
(∀𝑦Ⅎ𝑥𝜑 → Ⅎ𝑥[⦋𝑧 / 𝑥⦌𝐵 / 𝑦]𝜑) |
18 | 7, 10, 12, 17 | sbciedf 3765 |
. . 3
⊢
(∀𝑦Ⅎ𝑥𝜑 → ([𝑧 / 𝑥][𝐵 / 𝑦]𝜑 ↔ [⦋𝑧 / 𝑥⦌𝐵 / 𝑦]𝜑)) |
19 | 5, 18 | vtoclg 3510 |
. 2
⊢ (𝐴 ∈ 𝑉 → (∀𝑦Ⅎ𝑥𝜑 → ([𝐴 / 𝑥][𝐵 / 𝑦]𝜑 ↔ [⦋𝐴 / 𝑥⦌𝐵 / 𝑦]𝜑))) |
20 | 19 | imp 408 |
1
⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑦Ⅎ𝑥𝜑) → ([𝐴 / 𝑥][𝐵 / 𝑦]𝜑 ↔ [⦋𝐴 / 𝑥⦌𝐵 / 𝑦]𝜑)) |