Step | Hyp | Ref
| Expression |
1 | | df-ral 2305 |
. . . 4
⊢ (∀x ∈ A w ∈ B ↔ ∀x(x ∈ A → w ∈ B)) |
2 | | df-ral 2305 |
. . . . . 6
⊢ (∀x ∈ A B ∈ 𝐶 ↔ ∀x(x ∈ A → B ∈ 𝐶)) |
3 | | eleq2 2098 |
. . . . . . . . . . . . 13
⊢ (z = B →
(w ∈
z ↔ w ∈ B)) |
4 | 3 | biimprcd 149 |
. . . . . . . . . . . 12
⊢ (w ∈ B → (z =
B → w ∈ z)) |
5 | 4 | alrimiv 1751 |
. . . . . . . . . . 11
⊢ (w ∈ B → ∀z(z = B →
w ∈
z)) |
6 | | eqid 2037 |
. . . . . . . . . . . 12
⊢ B = B |
7 | | eqeq1 2043 |
. . . . . . . . . . . . . 14
⊢ (z = B →
(z = B
↔ B = B)) |
8 | 7, 3 | imbi12d 223 |
. . . . . . . . . . . . 13
⊢ (z = B →
((z = B
→ w ∈ z) ↔
(B = B
→ w ∈ B))) |
9 | 8 | spcgv 2634 |
. . . . . . . . . . . 12
⊢ (B ∈ 𝐶 → (∀z(z = B →
w ∈
z) → (B = B →
w ∈
B))) |
10 | 6, 9 | mpii 39 |
. . . . . . . . . . 11
⊢ (B ∈ 𝐶 → (∀z(z = B →
w ∈
z) → w ∈ B)) |
11 | 5, 10 | impbid2 131 |
. . . . . . . . . 10
⊢ (B ∈ 𝐶 → (w ∈ B ↔ ∀z(z = B →
w ∈
z))) |
12 | 11 | imim2i 12 |
. . . . . . . . 9
⊢
((x ∈ A →
B ∈ 𝐶) → (x ∈ A → (w
∈ B
↔ ∀z(z = B → w ∈ z)))) |
13 | 12 | pm5.74d 171 |
. . . . . . . 8
⊢
((x ∈ A →
B ∈ 𝐶) → ((x ∈ A → w ∈ B) ↔
(x ∈
A → ∀z(z = B →
w ∈
z)))) |
14 | 13 | alimi 1341 |
. . . . . . 7
⊢ (∀x(x ∈ A → B ∈ 𝐶) → ∀x((x ∈ A → w ∈ B) ↔
(x ∈
A → ∀z(z = B →
w ∈
z)))) |
15 | | albi 1354 |
. . . . . . 7
⊢ (∀x((x ∈ A → w ∈ B) ↔
(x ∈
A → ∀z(z = B →
w ∈
z))) → (∀x(x ∈ A → w ∈ B) ↔
∀x(x ∈ A →
∀z(z = B → w ∈ z)))) |
16 | 14, 15 | syl 14 |
. . . . . 6
⊢ (∀x(x ∈ A → B ∈ 𝐶) → (∀x(x ∈ A → w ∈ B) ↔
∀x(x ∈ A →
∀z(z = B → w ∈ z)))) |
17 | 2, 16 | sylbi 114 |
. . . . 5
⊢ (∀x ∈ A B ∈ 𝐶 → (∀x(x ∈ A → w ∈ B) ↔
∀x(x ∈ A →
∀z(z = B → w ∈ z)))) |
18 | | df-ral 2305 |
. . . . . . . 8
⊢ (∀x ∈ A (z = B →
w ∈
z) ↔ ∀x(x ∈ A → (z =
B → w ∈ z))) |
19 | 18 | albii 1356 |
. . . . . . 7
⊢ (∀z∀x ∈ A (z = B →
w ∈
z) ↔ ∀z∀x(x ∈ A → (z =
B → w ∈ z))) |
20 | | alcom 1364 |
. . . . . . 7
⊢ (∀x∀z(x ∈ A → (z =
B → w ∈ z)) ↔ ∀z∀x(x ∈ A → (z =
B → w ∈ z))) |
21 | 19, 20 | bitr4i 176 |
. . . . . 6
⊢ (∀z∀x ∈ A (z = B →
w ∈
z) ↔ ∀x∀z(x ∈ A → (z =
B → w ∈ z))) |
22 | | r19.23v 2419 |
. . . . . . . 8
⊢ (∀x ∈ A (z = B →
w ∈
z) ↔ (∃x ∈ A z = B →
w ∈
z)) |
23 | | vex 2554 |
. . . . . . . . . 10
⊢ z ∈
V |
24 | | eqeq1 2043 |
. . . . . . . . . . 11
⊢ (y = z →
(y = B
↔ z = B)) |
25 | 24 | rexbidv 2321 |
. . . . . . . . . 10
⊢ (y = z →
(∃x
∈ A
y = B
↔ ∃x ∈ A z = B)) |
26 | 23, 25 | elab 2681 |
. . . . . . . . 9
⊢ (z ∈ {y ∣ ∃x ∈ A y = B} ↔
∃x ∈ A z = B) |
27 | 26 | imbi1i 227 |
. . . . . . . 8
⊢
((z ∈ {y ∣
∃x ∈ A y = B} →
w ∈
z) ↔ (∃x ∈ A z = B →
w ∈
z)) |
28 | 22, 27 | bitr4i 176 |
. . . . . . 7
⊢ (∀x ∈ A (z = B →
w ∈
z) ↔ (z ∈ {y ∣ ∃x ∈ A y = B} →
w ∈
z)) |
29 | 28 | albii 1356 |
. . . . . 6
⊢ (∀z∀x ∈ A (z = B →
w ∈
z) ↔ ∀z(z ∈ {y ∣ ∃x ∈ A y = B} →
w ∈
z)) |
30 | | 19.21v 1750 |
. . . . . . 7
⊢ (∀z(x ∈ A → (z =
B → w ∈ z)) ↔ (x
∈ A
→ ∀z(z = B → w ∈ z))) |
31 | 30 | albii 1356 |
. . . . . 6
⊢ (∀x∀z(x ∈ A → (z =
B → w ∈ z)) ↔ ∀x(x ∈ A → ∀z(z = B →
w ∈
z))) |
32 | 21, 29, 31 | 3bitr3ri 200 |
. . . . 5
⊢ (∀x(x ∈ A → ∀z(z = B →
w ∈
z)) ↔ ∀z(z ∈ {y ∣ ∃x ∈ A y = B} →
w ∈
z)) |
33 | 17, 32 | syl6bb 185 |
. . . 4
⊢ (∀x ∈ A B ∈ 𝐶 → (∀x(x ∈ A → w ∈ B) ↔
∀z(z ∈ {y ∣
∃x ∈ A y = B} →
w ∈
z))) |
34 | 1, 33 | syl5bb 181 |
. . 3
⊢ (∀x ∈ A B ∈ 𝐶 → (∀x ∈ A w ∈ B ↔ ∀z(z ∈ {y ∣ ∃x ∈ A y = B} →
w ∈
z))) |
35 | 34 | abbidv 2152 |
. 2
⊢ (∀x ∈ A B ∈ 𝐶 → {w ∣ ∀x ∈ A w ∈ B} = {w ∣
∀z(z ∈ {y ∣
∃x ∈ A y = B} →
w ∈
z)}) |
36 | | df-iin 3651 |
. 2
⊢ ∩ x ∈ A B = {w ∣
∀x
∈ A
w ∈
B} |
37 | | df-int 3607 |
. 2
⊢ ∩ {y ∣ ∃x ∈ A y = B} =
{w ∣ ∀z(z ∈ {y ∣ ∃x ∈ A y = B} →
w ∈
z)} |
38 | 35, 36, 37 | 3eqtr4g 2094 |
1
⊢ (∀x ∈ A B ∈ 𝐶 → ∩ x ∈ A B = ∩ {y ∣ ∃x ∈ A y = B}) |