Step | Hyp | Ref
| Expression |
1 | | dfsbcq 3696 |
. . . . 5
⊢ (𝑧 = 𝐴 → ([𝑧 / 𝑥][𝐵 / 𝑦]𝜑 ↔ [𝐴 / 𝑥][𝐵 / 𝑦]𝜑)) |
2 | | csbeq1 3814 |
. . . . . 6
⊢ (𝑧 = 𝐴 → ⦋𝑧 / 𝑥⦌𝐵 = ⦋𝐴 / 𝑥⦌𝐵) |
3 | 2 | sbceq1d 3699 |
. . . . 5
⊢ (𝑧 = 𝐴 → ([⦋𝑧 / 𝑥⦌𝐵 / 𝑦]𝜑 ↔ [⦋𝐴 / 𝑥⦌𝐵 / 𝑦]𝜑)) |
4 | 1, 3 | bibi12d 349 |
. . . 4
⊢ (𝑧 = 𝐴 → (([𝑧 / 𝑥][𝐵 / 𝑦]𝜑 ↔ [⦋𝑧 / 𝑥⦌𝐵 / 𝑦]𝜑) ↔ ([𝐴 / 𝑥][𝐵 / 𝑦]𝜑 ↔ [⦋𝐴 / 𝑥⦌𝐵 / 𝑦]𝜑))) |
5 | 4 | imbi2d 344 |
. . 3
⊢ (𝑧 = 𝐴 → ((∀𝑦Ⅎ𝑥𝜑 → ([𝑧 / 𝑥][𝐵 / 𝑦]𝜑 ↔ [⦋𝑧 / 𝑥⦌𝐵 / 𝑦]𝜑)) ↔ (∀𝑦Ⅎ𝑥𝜑 → ([𝐴 / 𝑥][𝐵 / 𝑦]𝜑 ↔ [⦋𝐴 / 𝑥⦌𝐵 / 𝑦]𝜑)))) |
6 | | vex 3412 |
. . . . 5
⊢ 𝑧 ∈ V |
7 | 6 | a1i 11 |
. . . 4
⊢
(∀𝑦Ⅎ𝑥𝜑 → 𝑧 ∈ V) |
8 | | csbeq1a 3825 |
. . . . . 6
⊢ (𝑥 = 𝑧 → 𝐵 = ⦋𝑧 / 𝑥⦌𝐵) |
9 | 8 | sbceq1d 3699 |
. . . . 5
⊢ (𝑥 = 𝑧 → ([𝐵 / 𝑦]𝜑 ↔ [⦋𝑧 / 𝑥⦌𝐵 / 𝑦]𝜑)) |
10 | 9 | adantl 485 |
. . . 4
⊢
((∀𝑦Ⅎ𝑥𝜑 ∧ 𝑥 = 𝑧) → ([𝐵 / 𝑦]𝜑 ↔ [⦋𝑧 / 𝑥⦌𝐵 / 𝑦]𝜑)) |
11 | | nfnf1 2155 |
. . . . 5
⊢
Ⅎ𝑥Ⅎ𝑥𝜑 |
12 | 11 | nfal 2322 |
. . . 4
⊢
Ⅎ𝑥∀𝑦Ⅎ𝑥𝜑 |
13 | | nfa1 2152 |
. . . . 5
⊢
Ⅎ𝑦∀𝑦Ⅎ𝑥𝜑 |
14 | | nfcsb1v 3836 |
. . . . . 6
⊢
Ⅎ𝑥⦋𝑧 / 𝑥⦌𝐵 |
15 | 14 | a1i 11 |
. . . . 5
⊢
(∀𝑦Ⅎ𝑥𝜑 → Ⅎ𝑥⦋𝑧 / 𝑥⦌𝐵) |
16 | | sp 2180 |
. . . . 5
⊢
(∀𝑦Ⅎ𝑥𝜑 → Ⅎ𝑥𝜑) |
17 | 13, 15, 16 | nfsbcdw 3715 |
. . . 4
⊢
(∀𝑦Ⅎ𝑥𝜑 → Ⅎ𝑥[⦋𝑧 / 𝑥⦌𝐵 / 𝑦]𝜑) |
18 | 7, 10, 12, 17 | sbciedf 3738 |
. . 3
⊢
(∀𝑦Ⅎ𝑥𝜑 → ([𝑧 / 𝑥][𝐵 / 𝑦]𝜑 ↔ [⦋𝑧 / 𝑥⦌𝐵 / 𝑦]𝜑)) |
19 | 5, 18 | vtoclg 3481 |
. 2
⊢ (𝐴 ∈ 𝑉 → (∀𝑦Ⅎ𝑥𝜑 → ([𝐴 / 𝑥][𝐵 / 𝑦]𝜑 ↔ [⦋𝐴 / 𝑥⦌𝐵 / 𝑦]𝜑))) |
20 | 19 | imp 410 |
1
⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑦Ⅎ𝑥𝜑) → ([𝐴 / 𝑥][𝐵 / 𝑦]𝜑 ↔ [⦋𝐴 / 𝑥⦌𝐵 / 𝑦]𝜑)) |