Step | Hyp | Ref
| Expression |
1 | | csbabg 2901 |
. . 3
⊢ (A ∈ 𝑉 → ⦋A / x⦌{z ∣ ∃y(z ∈ y ∧ y ∈ B)} = {z ∣
[A / x]∃y(z ∈ y ∧ y ∈ B)}) |
2 | | sbcexg 2807 |
. . . . 5
⊢ (A ∈ 𝑉 → ([A / x]∃y(z ∈ y ∧ y ∈ B) ↔ ∃y[A /
x](z ∈ y ∧ y ∈ B))) |
3 | | sbcang 2800 |
. . . . . . 7
⊢ (A ∈ 𝑉 → ([A / x](z
∈ y ∧ y ∈ B) ↔
([A / x]z ∈ y ∧ [A /
x]y ∈ B))) |
4 | | sbcg 2821 |
. . . . . . . 8
⊢ (A ∈ 𝑉 → ([A / x]z ∈ y ↔
z ∈
y)) |
5 | | sbcel2g 2865 |
. . . . . . . 8
⊢ (A ∈ 𝑉 → ([A / x]y ∈ B ↔
y ∈
⦋A / x⦌B)) |
6 | 4, 5 | anbi12d 442 |
. . . . . . 7
⊢ (A ∈ 𝑉 → (([A / x]z ∈ y ∧ [A /
x]y ∈ B) ↔ (z
∈ y ∧ y ∈ ⦋A / x⦌B))) |
7 | 3, 6 | bitrd 177 |
. . . . . 6
⊢ (A ∈ 𝑉 → ([A / x](z
∈ y ∧ y ∈ B) ↔
(z ∈
y ∧
y ∈
⦋A / x⦌B))) |
8 | 7 | exbidv 1703 |
. . . . 5
⊢ (A ∈ 𝑉 → (∃y[A /
x](z ∈ y ∧ y ∈ B) ↔ ∃y(z ∈ y ∧ y ∈
⦋A / x⦌B))) |
9 | 2, 8 | bitrd 177 |
. . . 4
⊢ (A ∈ 𝑉 → ([A / x]∃y(z ∈ y ∧ y ∈ B) ↔ ∃y(z ∈ y ∧ y ∈
⦋A / x⦌B))) |
10 | 9 | abbidv 2152 |
. . 3
⊢ (A ∈ 𝑉 → {z ∣ [A / x]∃y(z ∈ y ∧ y ∈ B)} = {z ∣
∃y(z ∈ y ∧ y ∈ ⦋A / x⦌B)}) |
11 | 1, 10 | eqtrd 2069 |
. 2
⊢ (A ∈ 𝑉 → ⦋A / x⦌{z ∣ ∃y(z ∈ y ∧ y ∈ B)} = {z ∣
∃y(z ∈ y ∧ y ∈ ⦋A / x⦌B)}) |
12 | | df-uni 3572 |
. . 3
⊢ ∪ B = {z ∣ ∃y(z ∈ y ∧ y ∈ B)} |
13 | 12 | csbeq2i 2870 |
. 2
⊢
⦋A / x⦌∪
B = ⦋A / x⦌{z ∣ ∃y(z ∈ y ∧ y ∈ B)} |
14 | | df-uni 3572 |
. 2
⊢ ∪ ⦋A /
x⦌B = {z ∣
∃y(z ∈ y ∧ y ∈ ⦋A / x⦌B)} |
15 | 11, 13, 14 | 3eqtr4g 2094 |
1
⊢ (A ∈ 𝑉 → ⦋A / x⦌∪
B = ∪
⦋A / x⦌B) |