Step | Hyp | Ref
| Expression |
1 | | vex 3402 |
. . . . 5
⊢ 𝑦 ∈ V |
2 | | csbtt 3807 |
. . . . 5
⊢ ((𝑦 ∈ V ∧
Ⅎ𝑥𝐴) → ⦋𝑦 / 𝑥⦌𝐴 = 𝐴) |
3 | 1, 2 | mpan 690 |
. . . 4
⊢
(Ⅎ𝑥𝐴 → ⦋𝑦 / 𝑥⦌𝐴 = 𝐴) |
4 | | vex 3402 |
. . . . 5
⊢ 𝑧 ∈ V |
5 | | csbtt 3807 |
. . . . 5
⊢ ((𝑧 ∈ V ∧
Ⅎ𝑥𝐴) → ⦋𝑧 / 𝑥⦌𝐴 = 𝐴) |
6 | 4, 5 | mpan 690 |
. . . 4
⊢
(Ⅎ𝑥𝐴 → ⦋𝑧 / 𝑥⦌𝐴 = 𝐴) |
7 | 3, 6 | eqtr4d 2776 |
. . 3
⊢
(Ⅎ𝑥𝐴 → ⦋𝑦 / 𝑥⦌𝐴 = ⦋𝑧 / 𝑥⦌𝐴) |
8 | 7 | alrimivv 1935 |
. 2
⊢
(Ⅎ𝑥𝐴 → ∀𝑦∀𝑧⦋𝑦 / 𝑥⦌𝐴 = ⦋𝑧 / 𝑥⦌𝐴) |
9 | | nfv 1921 |
. . 3
⊢
Ⅎ𝑤∀𝑦∀𝑧⦋𝑦 / 𝑥⦌𝐴 = ⦋𝑧 / 𝑥⦌𝐴 |
10 | | eleq2 2821 |
. . . . . 6
⊢
(⦋𝑦 /
𝑥⦌𝐴 = ⦋𝑧 / 𝑥⦌𝐴 → (𝑤 ∈ ⦋𝑦 / 𝑥⦌𝐴 ↔ 𝑤 ∈ ⦋𝑧 / 𝑥⦌𝐴)) |
11 | | sbsbc 3684 |
. . . . . . 7
⊢ ([𝑦 / 𝑥]𝑤 ∈ 𝐴 ↔ [𝑦 / 𝑥]𝑤 ∈ 𝐴) |
12 | | sbcel2 4305 |
. . . . . . 7
⊢
([𝑦 / 𝑥]𝑤 ∈ 𝐴 ↔ 𝑤 ∈ ⦋𝑦 / 𝑥⦌𝐴) |
13 | 11, 12 | bitri 278 |
. . . . . 6
⊢ ([𝑦 / 𝑥]𝑤 ∈ 𝐴 ↔ 𝑤 ∈ ⦋𝑦 / 𝑥⦌𝐴) |
14 | | sbsbc 3684 |
. . . . . . 7
⊢ ([𝑧 / 𝑥]𝑤 ∈ 𝐴 ↔ [𝑧 / 𝑥]𝑤 ∈ 𝐴) |
15 | | sbcel2 4305 |
. . . . . . 7
⊢
([𝑧 / 𝑥]𝑤 ∈ 𝐴 ↔ 𝑤 ∈ ⦋𝑧 / 𝑥⦌𝐴) |
16 | 14, 15 | bitri 278 |
. . . . . 6
⊢ ([𝑧 / 𝑥]𝑤 ∈ 𝐴 ↔ 𝑤 ∈ ⦋𝑧 / 𝑥⦌𝐴) |
17 | 10, 13, 16 | 3bitr4g 317 |
. . . . 5
⊢
(⦋𝑦 /
𝑥⦌𝐴 = ⦋𝑧 / 𝑥⦌𝐴 → ([𝑦 / 𝑥]𝑤 ∈ 𝐴 ↔ [𝑧 / 𝑥]𝑤 ∈ 𝐴)) |
18 | 17 | 2alimi 1819 |
. . . 4
⊢
(∀𝑦∀𝑧⦋𝑦 / 𝑥⦌𝐴 = ⦋𝑧 / 𝑥⦌𝐴 → ∀𝑦∀𝑧([𝑦 / 𝑥]𝑤 ∈ 𝐴 ↔ [𝑧 / 𝑥]𝑤 ∈ 𝐴)) |
19 | | sbnf2 2359 |
. . . 4
⊢
(Ⅎ𝑥 𝑤 ∈ 𝐴 ↔ ∀𝑦∀𝑧([𝑦 / 𝑥]𝑤 ∈ 𝐴 ↔ [𝑧 / 𝑥]𝑤 ∈ 𝐴)) |
20 | 18, 19 | sylibr 237 |
. . 3
⊢
(∀𝑦∀𝑧⦋𝑦 / 𝑥⦌𝐴 = ⦋𝑧 / 𝑥⦌𝐴 → Ⅎ𝑥 𝑤 ∈ 𝐴) |
21 | 9, 20 | nfcd 2887 |
. 2
⊢
(∀𝑦∀𝑧⦋𝑦 / 𝑥⦌𝐴 = ⦋𝑧 / 𝑥⦌𝐴 → Ⅎ𝑥𝐴) |
22 | 8, 21 | impbii 212 |
1
⊢
(Ⅎ𝑥𝐴 ↔ ∀𝑦∀𝑧⦋𝑦 / 𝑥⦌𝐴 = ⦋𝑧 / 𝑥⦌𝐴) |