Step | Hyp | Ref
| Expression |
1 | | vex 2733 |
. . . . 5
⊢ 𝑦 ∈ V |
2 | | csbtt 3061 |
. . . . 5
⊢ ((𝑦 ∈ V ∧
Ⅎ𝑥𝐴) → ⦋𝑦 / 𝑥⦌𝐴 = 𝐴) |
3 | 1, 2 | mpan 422 |
. . . 4
⊢
(Ⅎ𝑥𝐴 → ⦋𝑦 / 𝑥⦌𝐴 = 𝐴) |
4 | | vex 2733 |
. . . . 5
⊢ 𝑧 ∈ V |
5 | | csbtt 3061 |
. . . . 5
⊢ ((𝑧 ∈ V ∧
Ⅎ𝑥𝐴) → ⦋𝑧 / 𝑥⦌𝐴 = 𝐴) |
6 | 4, 5 | mpan 422 |
. . . 4
⊢
(Ⅎ𝑥𝐴 → ⦋𝑧 / 𝑥⦌𝐴 = 𝐴) |
7 | 3, 6 | eqtr4d 2206 |
. . 3
⊢
(Ⅎ𝑥𝐴 → ⦋𝑦 / 𝑥⦌𝐴 = ⦋𝑧 / 𝑥⦌𝐴) |
8 | 7 | alrimivv 1868 |
. 2
⊢
(Ⅎ𝑥𝐴 → ∀𝑦∀𝑧⦋𝑦 / 𝑥⦌𝐴 = ⦋𝑧 / 𝑥⦌𝐴) |
9 | | nfv 1521 |
. . 3
⊢
Ⅎ𝑤∀𝑦∀𝑧⦋𝑦 / 𝑥⦌𝐴 = ⦋𝑧 / 𝑥⦌𝐴 |
10 | | eleq2 2234 |
. . . . . 6
⊢
(⦋𝑦 /
𝑥⦌𝐴 = ⦋𝑧 / 𝑥⦌𝐴 → (𝑤 ∈ ⦋𝑦 / 𝑥⦌𝐴 ↔ 𝑤 ∈ ⦋𝑧 / 𝑥⦌𝐴)) |
11 | | sbsbc 2959 |
. . . . . . 7
⊢ ([𝑦 / 𝑥]𝑤 ∈ 𝐴 ↔ [𝑦 / 𝑥]𝑤 ∈ 𝐴) |
12 | | sbcel2g 3070 |
. . . . . . . 8
⊢ (𝑦 ∈ V → ([𝑦 / 𝑥]𝑤 ∈ 𝐴 ↔ 𝑤 ∈ ⦋𝑦 / 𝑥⦌𝐴)) |
13 | 1, 12 | ax-mp 5 |
. . . . . . 7
⊢
([𝑦 / 𝑥]𝑤 ∈ 𝐴 ↔ 𝑤 ∈ ⦋𝑦 / 𝑥⦌𝐴) |
14 | 11, 13 | bitri 183 |
. . . . . 6
⊢ ([𝑦 / 𝑥]𝑤 ∈ 𝐴 ↔ 𝑤 ∈ ⦋𝑦 / 𝑥⦌𝐴) |
15 | | sbsbc 2959 |
. . . . . . 7
⊢ ([𝑧 / 𝑥]𝑤 ∈ 𝐴 ↔ [𝑧 / 𝑥]𝑤 ∈ 𝐴) |
16 | | sbcel2g 3070 |
. . . . . . . 8
⊢ (𝑧 ∈ V → ([𝑧 / 𝑥]𝑤 ∈ 𝐴 ↔ 𝑤 ∈ ⦋𝑧 / 𝑥⦌𝐴)) |
17 | 4, 16 | ax-mp 5 |
. . . . . . 7
⊢
([𝑧 / 𝑥]𝑤 ∈ 𝐴 ↔ 𝑤 ∈ ⦋𝑧 / 𝑥⦌𝐴) |
18 | 15, 17 | bitri 183 |
. . . . . 6
⊢ ([𝑧 / 𝑥]𝑤 ∈ 𝐴 ↔ 𝑤 ∈ ⦋𝑧 / 𝑥⦌𝐴) |
19 | 10, 14, 18 | 3bitr4g 222 |
. . . . 5
⊢
(⦋𝑦 /
𝑥⦌𝐴 = ⦋𝑧 / 𝑥⦌𝐴 → ([𝑦 / 𝑥]𝑤 ∈ 𝐴 ↔ [𝑧 / 𝑥]𝑤 ∈ 𝐴)) |
20 | 19 | 2alimi 1449 |
. . . 4
⊢
(∀𝑦∀𝑧⦋𝑦 / 𝑥⦌𝐴 = ⦋𝑧 / 𝑥⦌𝐴 → ∀𝑦∀𝑧([𝑦 / 𝑥]𝑤 ∈ 𝐴 ↔ [𝑧 / 𝑥]𝑤 ∈ 𝐴)) |
21 | | sbnf2 1974 |
. . . 4
⊢
(Ⅎ𝑥 𝑤 ∈ 𝐴 ↔ ∀𝑦∀𝑧([𝑦 / 𝑥]𝑤 ∈ 𝐴 ↔ [𝑧 / 𝑥]𝑤 ∈ 𝐴)) |
22 | 20, 21 | sylibr 133 |
. . 3
⊢
(∀𝑦∀𝑧⦋𝑦 / 𝑥⦌𝐴 = ⦋𝑧 / 𝑥⦌𝐴 → Ⅎ𝑥 𝑤 ∈ 𝐴) |
23 | 9, 22 | nfcd 2307 |
. 2
⊢
(∀𝑦∀𝑧⦋𝑦 / 𝑥⦌𝐴 = ⦋𝑧 / 𝑥⦌𝐴 → Ⅎ𝑥𝐴) |
24 | 8, 23 | impbii 125 |
1
⊢
(Ⅎ𝑥𝐴 ↔ ∀𝑦∀𝑧⦋𝑦 / 𝑥⦌𝐴 = ⦋𝑧 / 𝑥⦌𝐴) |