Step | Hyp | Ref
| Expression |
1 | | csbuni 4466 |
. . . 4
⊢
⦋𝐴 /
𝑥⦌∪ {𝑦
∣ (𝐹 “ {𝐵}) = {𝑦}} = ∪
⦋𝐴 / 𝑥⦌{𝑦 ∣ (𝐹 “ {𝐵}) = {𝑦}} |
2 | 1 | a1i 11 |
. . 3
⊢ (𝐴 ∈ 𝐶 → ⦋𝐴 / 𝑥⦌∪
{𝑦 ∣ (𝐹 “ {𝐵}) = {𝑦}} = ∪
⦋𝐴 / 𝑥⦌{𝑦 ∣ (𝐹 “ {𝐵}) = {𝑦}}) |
3 | | csbab 4008 |
. . . . . 6
⊢
⦋𝐴 /
𝑥⦌{𝑦 ∣ (𝐹 “ {𝐵}) = {𝑦}} = {𝑦 ∣ [𝐴 / 𝑥](𝐹 “ {𝐵}) = {𝑦}} |
4 | 3 | a1i 11 |
. . . . 5
⊢ (𝐴 ∈ 𝐶 → ⦋𝐴 / 𝑥⦌{𝑦 ∣ (𝐹 “ {𝐵}) = {𝑦}} = {𝑦 ∣ [𝐴 / 𝑥](𝐹 “ {𝐵}) = {𝑦}}) |
5 | | sbceqg 3984 |
. . . . . . 7
⊢ (𝐴 ∈ 𝐶 → ([𝐴 / 𝑥](𝐹 “ {𝐵}) = {𝑦} ↔ ⦋𝐴 / 𝑥⦌(𝐹 “ {𝐵}) = ⦋𝐴 / 𝑥⦌{𝑦})) |
6 | | csbima12 5483 |
. . . . . . . . . 10
⊢
⦋𝐴 /
𝑥⦌(𝐹 “ {𝐵}) = (⦋𝐴 / 𝑥⦌𝐹 “ ⦋𝐴 / 𝑥⦌{𝐵}) |
7 | 6 | a1i 11 |
. . . . . . . . 9
⊢ (𝐴 ∈ 𝐶 → ⦋𝐴 / 𝑥⦌(𝐹 “ {𝐵}) = (⦋𝐴 / 𝑥⦌𝐹 “ ⦋𝐴 / 𝑥⦌{𝐵})) |
8 | | csbsng 4243 |
. . . . . . . . . 10
⊢ (𝐴 ∈ 𝐶 → ⦋𝐴 / 𝑥⦌{𝐵} = {⦋𝐴 / 𝑥⦌𝐵}) |
9 | 8 | imaeq2d 5466 |
. . . . . . . . 9
⊢ (𝐴 ∈ 𝐶 → (⦋𝐴 / 𝑥⦌𝐹 “ ⦋𝐴 / 𝑥⦌{𝐵}) = (⦋𝐴 / 𝑥⦌𝐹 “ {⦋𝐴 / 𝑥⦌𝐵})) |
10 | 7, 9 | eqtrd 2656 |
. . . . . . . 8
⊢ (𝐴 ∈ 𝐶 → ⦋𝐴 / 𝑥⦌(𝐹 “ {𝐵}) = (⦋𝐴 / 𝑥⦌𝐹 “ {⦋𝐴 / 𝑥⦌𝐵})) |
11 | | csbconstg 3546 |
. . . . . . . 8
⊢ (𝐴 ∈ 𝐶 → ⦋𝐴 / 𝑥⦌{𝑦} = {𝑦}) |
12 | 10, 11 | eqeq12d 2637 |
. . . . . . 7
⊢ (𝐴 ∈ 𝐶 → (⦋𝐴 / 𝑥⦌(𝐹 “ {𝐵}) = ⦋𝐴 / 𝑥⦌{𝑦} ↔ (⦋𝐴 / 𝑥⦌𝐹 “ {⦋𝐴 / 𝑥⦌𝐵}) = {𝑦})) |
13 | 5, 12 | bitrd 268 |
. . . . . 6
⊢ (𝐴 ∈ 𝐶 → ([𝐴 / 𝑥](𝐹 “ {𝐵}) = {𝑦} ↔ (⦋𝐴 / 𝑥⦌𝐹 “ {⦋𝐴 / 𝑥⦌𝐵}) = {𝑦})) |
14 | 13 | abbidv 2741 |
. . . . 5
⊢ (𝐴 ∈ 𝐶 → {𝑦 ∣ [𝐴 / 𝑥](𝐹 “ {𝐵}) = {𝑦}} = {𝑦 ∣ (⦋𝐴 / 𝑥⦌𝐹 “ {⦋𝐴 / 𝑥⦌𝐵}) = {𝑦}}) |
15 | 4, 14 | eqtrd 2656 |
. . . 4
⊢ (𝐴 ∈ 𝐶 → ⦋𝐴 / 𝑥⦌{𝑦 ∣ (𝐹 “ {𝐵}) = {𝑦}} = {𝑦 ∣ (⦋𝐴 / 𝑥⦌𝐹 “ {⦋𝐴 / 𝑥⦌𝐵}) = {𝑦}}) |
16 | 15 | unieqd 4446 |
. . 3
⊢ (𝐴 ∈ 𝐶 → ∪
⦋𝐴 / 𝑥⦌{𝑦 ∣ (𝐹 “ {𝐵}) = {𝑦}} = ∪ {𝑦 ∣ (⦋𝐴 / 𝑥⦌𝐹 “ {⦋𝐴 / 𝑥⦌𝐵}) = {𝑦}}) |
17 | 2, 16 | eqtrd 2656 |
. 2
⊢ (𝐴 ∈ 𝐶 → ⦋𝐴 / 𝑥⦌∪
{𝑦 ∣ (𝐹 “ {𝐵}) = {𝑦}} = ∪ {𝑦 ∣ (⦋𝐴 / 𝑥⦌𝐹 “ {⦋𝐴 / 𝑥⦌𝐵}) = {𝑦}}) |
18 | | dffv4 6188 |
. . 3
⊢ (𝐹‘𝐵) = ∪ {𝑦 ∣ (𝐹 “ {𝐵}) = {𝑦}} |
19 | 18 | csbeq2i 3993 |
. 2
⊢
⦋𝐴 /
𝑥⦌(𝐹‘𝐵) = ⦋𝐴 / 𝑥⦌∪
{𝑦 ∣ (𝐹 “ {𝐵}) = {𝑦}} |
20 | | dffv4 6188 |
. 2
⊢
(⦋𝐴 /
𝑥⦌𝐹‘⦋𝐴 / 𝑥⦌𝐵) = ∪ {𝑦 ∣ (⦋𝐴 / 𝑥⦌𝐹 “ {⦋𝐴 / 𝑥⦌𝐵}) = {𝑦}} |
21 | 17, 19, 20 | 3eqtr4g 2681 |
1
⊢ (𝐴 ∈ 𝐶 → ⦋𝐴 / 𝑥⦌(𝐹‘𝐵) = (⦋𝐴 / 𝑥⦌𝐹‘⦋𝐴 / 𝑥⦌𝐵)) |