Proof of Theorem onfrALTlem4VD
Step | Hyp | Ref
| Expression |
1 | | vex 3343 |
. . 3
⊢ 𝑦 ∈ V |
2 | | sbcangOLD 39241 |
. . 3
⊢ (𝑦 ∈ V → ([𝑦 / 𝑥](𝑥 ∈ 𝑎 ∧ (𝑎 ∩ 𝑥) = ∅) ↔ ([𝑦 / 𝑥]𝑥 ∈ 𝑎 ∧ [𝑦 / 𝑥](𝑎 ∩ 𝑥) = ∅))) |
3 | 1, 2 | e0a 39501 |
. 2
⊢
([𝑦 / 𝑥](𝑥 ∈ 𝑎 ∧ (𝑎 ∩ 𝑥) = ∅) ↔ ([𝑦 / 𝑥]𝑥 ∈ 𝑎 ∧ [𝑦 / 𝑥](𝑎 ∩ 𝑥) = ∅)) |
4 | | sbcel1gvOLD 39593 |
. . . 4
⊢ (𝑦 ∈ V → ([𝑦 / 𝑥]𝑥 ∈ 𝑎 ↔ 𝑦 ∈ 𝑎)) |
5 | 1, 4 | e0a 39501 |
. . 3
⊢
([𝑦 / 𝑥]𝑥 ∈ 𝑎 ↔ 𝑦 ∈ 𝑎) |
6 | | sbceqg 4127 |
. . . . 5
⊢ (𝑦 ∈ V → ([𝑦 / 𝑥](𝑎 ∩ 𝑥) = ∅ ↔ ⦋𝑦 / 𝑥⦌(𝑎 ∩ 𝑥) = ⦋𝑦 / 𝑥⦌∅)) |
7 | 1, 6 | e0a 39501 |
. . . 4
⊢
([𝑦 / 𝑥](𝑎 ∩ 𝑥) = ∅ ↔ ⦋𝑦 / 𝑥⦌(𝑎 ∩ 𝑥) = ⦋𝑦 / 𝑥⦌∅) |
8 | | csbingOLD 39554 |
. . . . . . 7
⊢ (𝑦 ∈ V →
⦋𝑦 / 𝑥⦌(𝑎 ∩ 𝑥) = (⦋𝑦 / 𝑥⦌𝑎 ∩ ⦋𝑦 / 𝑥⦌𝑥)) |
9 | 1, 8 | e0a 39501 |
. . . . . 6
⊢
⦋𝑦 /
𝑥⦌(𝑎 ∩ 𝑥) = (⦋𝑦 / 𝑥⦌𝑎 ∩ ⦋𝑦 / 𝑥⦌𝑥) |
10 | | csbconstg 3687 |
. . . . . . . 8
⊢ (𝑦 ∈ V →
⦋𝑦 / 𝑥⦌𝑎 = 𝑎) |
11 | 1, 10 | e0a 39501 |
. . . . . . 7
⊢
⦋𝑦 /
𝑥⦌𝑎 = 𝑎 |
12 | | csbvarg 4146 |
. . . . . . . 8
⊢ (𝑦 ∈ V →
⦋𝑦 / 𝑥⦌𝑥 = 𝑦) |
13 | 1, 12 | e0a 39501 |
. . . . . . 7
⊢
⦋𝑦 /
𝑥⦌𝑥 = 𝑦 |
14 | 11, 13 | ineq12i 3955 |
. . . . . 6
⊢
(⦋𝑦 /
𝑥⦌𝑎 ∩ ⦋𝑦 / 𝑥⦌𝑥) = (𝑎 ∩ 𝑦) |
15 | 9, 14 | eqtri 2782 |
. . . . 5
⊢
⦋𝑦 /
𝑥⦌(𝑎 ∩ 𝑥) = (𝑎 ∩ 𝑦) |
16 | | csbconstg 3687 |
. . . . . 6
⊢ (𝑦 ∈ V →
⦋𝑦 / 𝑥⦌∅ =
∅) |
17 | 1, 16 | e0a 39501 |
. . . . 5
⊢
⦋𝑦 /
𝑥⦌∅ =
∅ |
18 | 15, 17 | eqeq12i 2774 |
. . . 4
⊢
(⦋𝑦 /
𝑥⦌(𝑎 ∩ 𝑥) = ⦋𝑦 / 𝑥⦌∅ ↔ (𝑎 ∩ 𝑦) = ∅) |
19 | 7, 18 | bitri 264 |
. . 3
⊢
([𝑦 / 𝑥](𝑎 ∩ 𝑥) = ∅ ↔ (𝑎 ∩ 𝑦) = ∅) |
20 | 5, 19 | anbi12i 735 |
. 2
⊢
(([𝑦 / 𝑥]𝑥 ∈ 𝑎 ∧ [𝑦 / 𝑥](𝑎 ∩ 𝑥) = ∅) ↔ (𝑦 ∈ 𝑎 ∧ (𝑎 ∩ 𝑦) = ∅)) |
21 | 3, 20 | bitri 264 |
1
⊢
([𝑦 / 𝑥](𝑥 ∈ 𝑎 ∧ (𝑎 ∩ 𝑥) = ∅) ↔ (𝑦 ∈ 𝑎 ∧ (𝑎 ∩ 𝑦) = ∅)) |