Step | Hyp | Ref
| Expression |
1 | | csbab 4327 |
. . . 4
⊢
⦋𝐴 /
𝑥⦌{𝑧 ∣ ∃𝑦(𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵)} = {𝑧 ∣ [𝐴 / 𝑥]∃𝑦(𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵)} |
2 | | sbcex2 3743 |
. . . . . 6
⊢
([𝐴 / 𝑥]∃𝑦(𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵) ↔ ∃𝑦[𝐴 / 𝑥](𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵)) |
3 | | sbcan 3730 |
. . . . . . . 8
⊢
([𝐴 / 𝑥](𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵) ↔ ([𝐴 / 𝑥]𝑧 ∈ 𝑦 ∧ [𝐴 / 𝑥]𝑦 ∈ 𝐵)) |
4 | | sbcg 3755 |
. . . . . . . . . 10
⊢ (𝐴 ∈ V → ([𝐴 / 𝑥]𝑧 ∈ 𝑦 ↔ 𝑧 ∈ 𝑦)) |
5 | 4 | anbi1d 633 |
. . . . . . . . 9
⊢ (𝐴 ∈ V → (([𝐴 / 𝑥]𝑧 ∈ 𝑦 ∧ [𝐴 / 𝑥]𝑦 ∈ 𝐵) ↔ (𝑧 ∈ 𝑦 ∧ [𝐴 / 𝑥]𝑦 ∈ 𝐵))) |
6 | | sbcel2 4305 |
. . . . . . . . . 10
⊢
([𝐴 / 𝑥]𝑦 ∈ 𝐵 ↔ 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐵) |
7 | 6 | anbi2i 626 |
. . . . . . . . 9
⊢ ((𝑧 ∈ 𝑦 ∧ [𝐴 / 𝑥]𝑦 ∈ 𝐵) ↔ (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐵)) |
8 | 5, 7 | bitrdi 290 |
. . . . . . . 8
⊢ (𝐴 ∈ V → (([𝐴 / 𝑥]𝑧 ∈ 𝑦 ∧ [𝐴 / 𝑥]𝑦 ∈ 𝐵) ↔ (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐵))) |
9 | 3, 8 | syl5bb 286 |
. . . . . . 7
⊢ (𝐴 ∈ V → ([𝐴 / 𝑥](𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵) ↔ (𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐵))) |
10 | 9 | exbidv 1928 |
. . . . . 6
⊢ (𝐴 ∈ V → (∃𝑦[𝐴 / 𝑥](𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵) ↔ ∃𝑦(𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐵))) |
11 | 2, 10 | syl5bb 286 |
. . . . 5
⊢ (𝐴 ∈ V → ([𝐴 / 𝑥]∃𝑦(𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵) ↔ ∃𝑦(𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐵))) |
12 | 11 | abbidv 2802 |
. . . 4
⊢ (𝐴 ∈ V → {𝑧 ∣ [𝐴 / 𝑥]∃𝑦(𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵)} = {𝑧 ∣ ∃𝑦(𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐵)}) |
13 | 1, 12 | syl5eq 2785 |
. . 3
⊢ (𝐴 ∈ V →
⦋𝐴 / 𝑥⦌{𝑧 ∣ ∃𝑦(𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵)} = {𝑧 ∣ ∃𝑦(𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐵)}) |
14 | | df-uni 4797 |
. . . 4
⊢ ∪ 𝐵 =
{𝑧 ∣ ∃𝑦(𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵)} |
15 | 14 | csbeq2i 3798 |
. . 3
⊢
⦋𝐴 /
𝑥⦌∪ 𝐵 =
⦋𝐴 / 𝑥⦌{𝑧 ∣ ∃𝑦(𝑧 ∈ 𝑦 ∧ 𝑦 ∈ 𝐵)} |
16 | | df-uni 4797 |
. . 3
⊢ ∪ ⦋𝐴 / 𝑥⦌𝐵 = {𝑧 ∣ ∃𝑦(𝑧 ∈ 𝑦 ∧ 𝑦 ∈ ⦋𝐴 / 𝑥⦌𝐵)} |
17 | 13, 15, 16 | 3eqtr4g 2798 |
. 2
⊢ (𝐴 ∈ V →
⦋𝐴 / 𝑥⦌∪ 𝐵 =
∪ ⦋𝐴 / 𝑥⦌𝐵) |
18 | | csbprc 4295 |
. . 3
⊢ (¬
𝐴 ∈ V →
⦋𝐴 / 𝑥⦌∪ 𝐵 =
∅) |
19 | | csbprc 4295 |
. . . . 5
⊢ (¬
𝐴 ∈ V →
⦋𝐴 / 𝑥⦌𝐵 = ∅) |
20 | 19 | unieqd 4810 |
. . . 4
⊢ (¬
𝐴 ∈ V → ∪ ⦋𝐴 / 𝑥⦌𝐵 = ∪
∅) |
21 | | uni0 4826 |
. . . 4
⊢ ∪ ∅ = ∅ |
22 | 20, 21 | eqtr2di 2790 |
. . 3
⊢ (¬
𝐴 ∈ V → ∅ =
∪ ⦋𝐴 / 𝑥⦌𝐵) |
23 | 18, 22 | eqtrd 2773 |
. 2
⊢ (¬
𝐴 ∈ V →
⦋𝐴 / 𝑥⦌∪ 𝐵 =
∪ ⦋𝐴 / 𝑥⦌𝐵) |
24 | 17, 23 | pm2.61i 185 |
1
⊢
⦋𝐴 /
𝑥⦌∪ 𝐵 =
∪ ⦋𝐴 / 𝑥⦌𝐵 |