Step | Hyp | Ref
| Expression |
1 | | csbeq1 3834 |
. . . 4
⊢ (𝑦 = 𝐴 → ⦋𝑦 / 𝑥⦌(𝐵 ∖ 𝐶) = ⦋𝐴 / 𝑥⦌(𝐵 ∖ 𝐶)) |
2 | | csbeq1 3834 |
. . . . 5
⊢ (𝑦 = 𝐴 → ⦋𝑦 / 𝑥⦌𝐵 = ⦋𝐴 / 𝑥⦌𝐵) |
3 | | csbeq1 3834 |
. . . . 5
⊢ (𝑦 = 𝐴 → ⦋𝑦 / 𝑥⦌𝐶 = ⦋𝐴 / 𝑥⦌𝐶) |
4 | 2, 3 | difeq12d 4057 |
. . . 4
⊢ (𝑦 = 𝐴 → (⦋𝑦 / 𝑥⦌𝐵 ∖ ⦋𝑦 / 𝑥⦌𝐶) = (⦋𝐴 / 𝑥⦌𝐵 ∖ ⦋𝐴 / 𝑥⦌𝐶)) |
5 | 1, 4 | eqeq12d 2754 |
. . 3
⊢ (𝑦 = 𝐴 → (⦋𝑦 / 𝑥⦌(𝐵 ∖ 𝐶) = (⦋𝑦 / 𝑥⦌𝐵 ∖ ⦋𝑦 / 𝑥⦌𝐶) ↔ ⦋𝐴 / 𝑥⦌(𝐵 ∖ 𝐶) = (⦋𝐴 / 𝑥⦌𝐵 ∖ ⦋𝐴 / 𝑥⦌𝐶))) |
6 | | vex 3433 |
. . . 4
⊢ 𝑦 ∈ V |
7 | | nfcsb1v 3856 |
. . . . 5
⊢
Ⅎ𝑥⦋𝑦 / 𝑥⦌𝐵 |
8 | | nfcsb1v 3856 |
. . . . 5
⊢
Ⅎ𝑥⦋𝑦 / 𝑥⦌𝐶 |
9 | 7, 8 | nfdif 4059 |
. . . 4
⊢
Ⅎ𝑥(⦋𝑦 / 𝑥⦌𝐵 ∖ ⦋𝑦 / 𝑥⦌𝐶) |
10 | | csbeq1a 3845 |
. . . . 5
⊢ (𝑥 = 𝑦 → 𝐵 = ⦋𝑦 / 𝑥⦌𝐵) |
11 | | csbeq1a 3845 |
. . . . 5
⊢ (𝑥 = 𝑦 → 𝐶 = ⦋𝑦 / 𝑥⦌𝐶) |
12 | 10, 11 | difeq12d 4057 |
. . . 4
⊢ (𝑥 = 𝑦 → (𝐵 ∖ 𝐶) = (⦋𝑦 / 𝑥⦌𝐵 ∖ ⦋𝑦 / 𝑥⦌𝐶)) |
13 | 6, 9, 12 | csbief 3866 |
. . 3
⊢
⦋𝑦 /
𝑥⦌(𝐵 ∖ 𝐶) = (⦋𝑦 / 𝑥⦌𝐵 ∖ ⦋𝑦 / 𝑥⦌𝐶) |
14 | 5, 13 | vtoclg 3502 |
. 2
⊢ (𝐴 ∈ V →
⦋𝐴 / 𝑥⦌(𝐵 ∖ 𝐶) = (⦋𝐴 / 𝑥⦌𝐵 ∖ ⦋𝐴 / 𝑥⦌𝐶)) |
15 | | dif0 4306 |
. . . 4
⊢ (∅
∖ ∅) = ∅ |
16 | 15 | a1i 11 |
. . 3
⊢ (¬
𝐴 ∈ V → (∅
∖ ∅) = ∅) |
17 | | csbprc 4340 |
. . . 4
⊢ (¬
𝐴 ∈ V →
⦋𝐴 / 𝑥⦌𝐵 = ∅) |
18 | | csbprc 4340 |
. . . 4
⊢ (¬
𝐴 ∈ V →
⦋𝐴 / 𝑥⦌𝐶 = ∅) |
19 | 17, 18 | difeq12d 4057 |
. . 3
⊢ (¬
𝐴 ∈ V →
(⦋𝐴 / 𝑥⦌𝐵 ∖ ⦋𝐴 / 𝑥⦌𝐶) = (∅ ∖
∅)) |
20 | | csbprc 4340 |
. . 3
⊢ (¬
𝐴 ∈ V →
⦋𝐴 / 𝑥⦌(𝐵 ∖ 𝐶) = ∅) |
21 | 16, 19, 20 | 3eqtr4rd 2789 |
. 2
⊢ (¬
𝐴 ∈ V →
⦋𝐴 / 𝑥⦌(𝐵 ∖ 𝐶) = (⦋𝐴 / 𝑥⦌𝐵 ∖ ⦋𝐴 / 𝑥⦌𝐶)) |
22 | 14, 21 | pm2.61i 182 |
1
⊢
⦋𝐴 /
𝑥⦌(𝐵 ∖ 𝐶) = (⦋𝐴 / 𝑥⦌𝐵 ∖ ⦋𝐴 / 𝑥⦌𝐶) |