Proof of Theorem onfrALTlem4VD
Step | Hyp | Ref
| Expression |
1 | | vex 3203 |
. . 3
⊢ 𝑦 ∈ V |
2 | | sbcangOLD 38739 |
. . 3
⊢ (𝑦 ∈ V → ([𝑦 / 𝑥](𝑥 ∈ 𝑎 ∧ (𝑎 ∩ 𝑥) = ∅) ↔ ([𝑦 / 𝑥]𝑥 ∈ 𝑎 ∧ [𝑦 / 𝑥](𝑎 ∩ 𝑥) = ∅))) |
3 | 1, 2 | e0a 38999 |
. 2
⊢
([𝑦 / 𝑥](𝑥 ∈ 𝑎 ∧ (𝑎 ∩ 𝑥) = ∅) ↔ ([𝑦 / 𝑥]𝑥 ∈ 𝑎 ∧ [𝑦 / 𝑥](𝑎 ∩ 𝑥) = ∅)) |
4 | | sbcel1gvOLD 39094 |
. . . 4
⊢ (𝑦 ∈ V → ([𝑦 / 𝑥]𝑥 ∈ 𝑎 ↔ 𝑦 ∈ 𝑎)) |
5 | 1, 4 | e0a 38999 |
. . 3
⊢
([𝑦 / 𝑥]𝑥 ∈ 𝑎 ↔ 𝑦 ∈ 𝑎) |
6 | | sbceqg 3984 |
. . . . 5
⊢ (𝑦 ∈ V → ([𝑦 / 𝑥](𝑎 ∩ 𝑥) = ∅ ↔ ⦋𝑦 / 𝑥⦌(𝑎 ∩ 𝑥) = ⦋𝑦 / 𝑥⦌∅)) |
7 | 1, 6 | e0a 38999 |
. . . 4
⊢
([𝑦 / 𝑥](𝑎 ∩ 𝑥) = ∅ ↔ ⦋𝑦 / 𝑥⦌(𝑎 ∩ 𝑥) = ⦋𝑦 / 𝑥⦌∅) |
8 | | csbingOLD 39054 |
. . . . . . 7
⊢ (𝑦 ∈ V →
⦋𝑦 / 𝑥⦌(𝑎 ∩ 𝑥) = (⦋𝑦 / 𝑥⦌𝑎 ∩ ⦋𝑦 / 𝑥⦌𝑥)) |
9 | 1, 8 | e0a 38999 |
. . . . . 6
⊢
⦋𝑦 /
𝑥⦌(𝑎 ∩ 𝑥) = (⦋𝑦 / 𝑥⦌𝑎 ∩ ⦋𝑦 / 𝑥⦌𝑥) |
10 | | csbconstg 3546 |
. . . . . . . 8
⊢ (𝑦 ∈ V →
⦋𝑦 / 𝑥⦌𝑎 = 𝑎) |
11 | 1, 10 | e0a 38999 |
. . . . . . 7
⊢
⦋𝑦 /
𝑥⦌𝑎 = 𝑎 |
12 | | csbvarg 4003 |
. . . . . . . 8
⊢ (𝑦 ∈ V →
⦋𝑦 / 𝑥⦌𝑥 = 𝑦) |
13 | 1, 12 | e0a 38999 |
. . . . . . 7
⊢
⦋𝑦 /
𝑥⦌𝑥 = 𝑦 |
14 | 11, 13 | ineq12i 3812 |
. . . . . 6
⊢
(⦋𝑦 /
𝑥⦌𝑎 ∩ ⦋𝑦 / 𝑥⦌𝑥) = (𝑎 ∩ 𝑦) |
15 | 9, 14 | eqtri 2644 |
. . . . 5
⊢
⦋𝑦 /
𝑥⦌(𝑎 ∩ 𝑥) = (𝑎 ∩ 𝑦) |
16 | | csbconstg 3546 |
. . . . . 6
⊢ (𝑦 ∈ V →
⦋𝑦 / 𝑥⦌∅ =
∅) |
17 | 1, 16 | e0a 38999 |
. . . . 5
⊢
⦋𝑦 /
𝑥⦌∅ =
∅ |
18 | 15, 17 | eqeq12i 2636 |
. . . 4
⊢
(⦋𝑦 /
𝑥⦌(𝑎 ∩ 𝑥) = ⦋𝑦 / 𝑥⦌∅ ↔ (𝑎 ∩ 𝑦) = ∅) |
19 | 7, 18 | bitri 264 |
. . 3
⊢
([𝑦 / 𝑥](𝑎 ∩ 𝑥) = ∅ ↔ (𝑎 ∩ 𝑦) = ∅) |
20 | 5, 19 | anbi12i 733 |
. 2
⊢
(([𝑦 / 𝑥]𝑥 ∈ 𝑎 ∧ [𝑦 / 𝑥](𝑎 ∩ 𝑥) = ∅) ↔ (𝑦 ∈ 𝑎 ∧ (𝑎 ∩ 𝑦) = ∅)) |
21 | 3, 20 | bitri 264 |
1
⊢
([𝑦 / 𝑥](𝑥 ∈ 𝑎 ∧ (𝑎 ∩ 𝑥) = ∅) ↔ (𝑦 ∈ 𝑎 ∧ (𝑎 ∩ 𝑦) = ∅)) |