Step | Hyp | Ref
| Expression |
1 | | eluni 3574 |
. . . . . 6
⊢ (u ∈ ∪ A ↔ ∃y(u ∈ y ∧ y ∈ A)) |
2 | 1 | anbi2i 430 |
. . . . 5
⊢
((z ∈ u ∧ u ∈ ∪ A) ↔ (z
∈ u ∧ ∃y(u ∈ y ∧ y ∈ A))) |
3 | 2 | exbii 1493 |
. . . 4
⊢ (∃u(z ∈ u ∧ u ∈ ∪ A) ↔ ∃u(z ∈ u ∧ ∃y(u ∈ y ∧ y ∈ A))) |
4 | | 19.42v 1783 |
. . . . . . 7
⊢ (∃y(z ∈ u ∧ (u ∈ y ∧ y ∈ A)) ↔ (z
∈ u ∧ ∃y(u ∈ y ∧ y ∈ A))) |
5 | 4 | bicomi 123 |
. . . . . 6
⊢
((z ∈ u ∧ ∃y(u ∈ y ∧ y ∈ A)) ↔
∃y(z ∈ u ∧ (u ∈ y ∧ y ∈ A))) |
6 | 5 | exbii 1493 |
. . . . 5
⊢ (∃u(z ∈ u ∧ ∃y(u ∈ y ∧ y ∈ A)) ↔ ∃u∃y(z ∈ u ∧ (u ∈ y ∧ y ∈ A))) |
7 | | excom 1551 |
. . . . . 6
⊢ (∃u∃y(z ∈ u ∧ (u ∈ y ∧ y ∈ A)) ↔ ∃y∃u(z ∈ u ∧ (u ∈ y ∧ y ∈ A))) |
8 | | anass 381 |
. . . . . . . 8
⊢
(((z ∈ u ∧ u ∈ y) ∧ y ∈ A) ↔
(z ∈
u ∧
(u ∈
y ∧
y ∈
A))) |
9 | | ancom 253 |
. . . . . . . 8
⊢
(((z ∈ u ∧ u ∈ y) ∧ y ∈ A) ↔
(y ∈
A ∧
(z ∈
u ∧
u ∈
y))) |
10 | 8, 9 | bitr3i 175 |
. . . . . . 7
⊢
((z ∈ u ∧ (u ∈ y ∧ y ∈ A)) ↔
(y ∈
A ∧
(z ∈
u ∧
u ∈
y))) |
11 | 10 | 2exbii 1494 |
. . . . . 6
⊢ (∃y∃u(z ∈ u ∧ (u ∈ y ∧ y ∈ A)) ↔ ∃y∃u(y ∈ A ∧ (z ∈ u ∧ u ∈ y))) |
12 | | exdistr 1784 |
. . . . . 6
⊢ (∃y∃u(y ∈ A ∧ (z ∈ u ∧ u ∈ y)) ↔ ∃y(y ∈ A ∧ ∃u(z ∈ u ∧ u ∈ y))) |
13 | 7, 11, 12 | 3bitri 195 |
. . . . 5
⊢ (∃u∃y(z ∈ u ∧ (u ∈ y ∧ y ∈ A)) ↔ ∃y(y ∈ A ∧ ∃u(z ∈ u ∧ u ∈ y))) |
14 | | eluni 3574 |
. . . . . . . 8
⊢ (z ∈ ∪ y ↔ ∃u(z ∈ u ∧ u ∈ y)) |
15 | 14 | bicomi 123 |
. . . . . . 7
⊢ (∃u(z ∈ u ∧ u ∈ y) ↔ z
∈ ∪ y) |
16 | 15 | anbi2i 430 |
. . . . . 6
⊢
((y ∈ A ∧ ∃u(z ∈ u ∧ u ∈ y)) ↔
(y ∈
A ∧
z ∈ ∪ y)) |
17 | 16 | exbii 1493 |
. . . . 5
⊢ (∃y(y ∈ A ∧ ∃u(z ∈ u ∧ u ∈ y)) ↔ ∃y(y ∈ A ∧ z ∈ ∪ y)) |
18 | 6, 13, 17 | 3bitri 195 |
. . . 4
⊢ (∃u(z ∈ u ∧ ∃y(u ∈ y ∧ y ∈ A)) ↔ ∃y(y ∈ A ∧ z ∈ ∪ y)) |
19 | | vex 2554 |
. . . . . . . . . . 11
⊢ y ∈
V |
20 | 19 | uniex 4140 |
. . . . . . . . . 10
⊢ ∪ y ∈ V |
21 | | eleq2 2098 |
. . . . . . . . . 10
⊢ (v = ∪ y → (z
∈ v
↔ z ∈ ∪ y)) |
22 | 20, 21 | ceqsexv 2587 |
. . . . . . . . 9
⊢ (∃v(v = ∪ y ∧ z ∈ v) ↔ z
∈ ∪ y) |
23 | | exancom 1496 |
. . . . . . . . 9
⊢ (∃v(v = ∪ y ∧ z ∈ v) ↔ ∃v(z ∈ v ∧ v = ∪ y)) |
24 | 22, 23 | bitr3i 175 |
. . . . . . . 8
⊢ (z ∈ ∪ y ↔ ∃v(z ∈ v ∧ v = ∪ y)) |
25 | 24 | anbi2i 430 |
. . . . . . 7
⊢
((y ∈ A ∧ z ∈ ∪ y) ↔ (y
∈ A ∧ ∃v(z ∈ v ∧ v = ∪ y))) |
26 | | 19.42v 1783 |
. . . . . . 7
⊢ (∃v(y ∈ A ∧ (z ∈ v ∧ v = ∪ y)) ↔ (y
∈ A ∧ ∃v(z ∈ v ∧ v = ∪ y))) |
27 | | ancom 253 |
. . . . . . . . 9
⊢
((y ∈ A ∧ (z ∈ v ∧ v = ∪ y)) ↔
((z ∈
v ∧
v = ∪ y) ∧ y ∈ A)) |
28 | | anass 381 |
. . . . . . . . 9
⊢
(((z ∈ v ∧ v = ∪ y) ∧ y ∈ A) ↔
(z ∈
v ∧
(v = ∪ y ∧ y ∈ A))) |
29 | 27, 28 | bitri 173 |
. . . . . . . 8
⊢
((y ∈ A ∧ (z ∈ v ∧ v = ∪ y)) ↔ (z ∈ v ∧ (v = ∪ y ∧ y ∈ A))) |
30 | 29 | exbii 1493 |
. . . . . . 7
⊢ (∃v(y ∈ A ∧ (z ∈ v ∧ v = ∪ y)) ↔ ∃v(z ∈ v ∧ (v = ∪ y ∧ y ∈ A))) |
31 | 25, 26, 30 | 3bitr2i 197 |
. . . . . 6
⊢
((y ∈ A ∧ z ∈ ∪ y) ↔ ∃v(z ∈ v ∧ (v = ∪ y ∧ y ∈ A))) |
32 | 31 | exbii 1493 |
. . . . 5
⊢ (∃y(y ∈ A ∧ z ∈ ∪ y) ↔ ∃y∃v(z ∈ v ∧ (v = ∪ y ∧ y ∈ A))) |
33 | | excom 1551 |
. . . . 5
⊢ (∃y∃v(z ∈ v ∧ (v = ∪ y ∧ y ∈ A)) ↔ ∃v∃y(z ∈ v ∧ (v = ∪ y ∧ y ∈ A))) |
34 | | exdistr 1784 |
. . . . . 6
⊢ (∃v∃y(z ∈ v ∧ (v = ∪ y ∧ y ∈ A)) ↔ ∃v(z ∈ v ∧ ∃y(v = ∪ y ∧ y ∈ A))) |
35 | | vex 2554 |
. . . . . . . . . 10
⊢ v ∈
V |
36 | | eqeq1 2043 |
. . . . . . . . . . . 12
⊢ (x = v →
(x = ∪ y ↔ v =
∪ y)) |
37 | 36 | anbi1d 438 |
. . . . . . . . . . 11
⊢ (x = v →
((x = ∪ y ∧ y ∈ A) ↔ (v =
∪ y ∧ y ∈ A))) |
38 | 37 | exbidv 1703 |
. . . . . . . . . 10
⊢ (x = v →
(∃y(x = ∪ y ∧ y ∈ A) ↔
∃y(v = ∪ y ∧ y ∈ A))) |
39 | 35, 38 | elab 2681 |
. . . . . . . . 9
⊢ (v ∈ {x ∣ ∃y(x = ∪ y ∧ y ∈ A)} ↔ ∃y(v = ∪ y ∧ y ∈ A)) |
40 | 39 | bicomi 123 |
. . . . . . . 8
⊢ (∃y(v = ∪ y ∧ y ∈ A) ↔ v
∈ {x
∣ ∃y(x = ∪ y ∧ y ∈ A)}) |
41 | 40 | anbi2i 430 |
. . . . . . 7
⊢
((z ∈ v ∧ ∃y(v = ∪ y ∧ y ∈ A)) ↔
(z ∈
v ∧
v ∈
{x ∣ ∃y(x = ∪ y ∧ y ∈ A)})) |
42 | 41 | exbii 1493 |
. . . . . 6
⊢ (∃v(z ∈ v ∧ ∃y(v = ∪ y ∧ y ∈ A)) ↔ ∃v(z ∈ v ∧ v ∈ {x ∣ ∃y(x = ∪ y ∧ y ∈ A)})) |
43 | 34, 42 | bitri 173 |
. . . . 5
⊢ (∃v∃y(z ∈ v ∧ (v = ∪ y ∧ y ∈ A)) ↔ ∃v(z ∈ v ∧ v ∈ {x ∣ ∃y(x = ∪ y ∧ y ∈ A)})) |
44 | 32, 33, 43 | 3bitri 195 |
. . . 4
⊢ (∃y(y ∈ A ∧ z ∈ ∪ y) ↔ ∃v(z ∈ v ∧ v ∈ {x ∣ ∃y(x = ∪ y ∧ y ∈ A)})) |
45 | 3, 18, 44 | 3bitri 195 |
. . 3
⊢ (∃u(z ∈ u ∧ u ∈ ∪ A) ↔ ∃v(z ∈ v ∧ v ∈ {x ∣ ∃y(x = ∪ y ∧ y ∈ A)})) |
46 | 45 | abbii 2150 |
. 2
⊢ {z ∣ ∃u(z ∈ u ∧ u ∈ ∪ A)} = {z ∣ ∃v(z ∈ v ∧ v ∈ {x ∣ ∃y(x = ∪ y ∧ y ∈ A)})} |
47 | | df-uni 3572 |
. 2
⊢ ∪ ∪ A = {z ∣
∃u(z ∈ u ∧ u ∈ ∪ A)} |
48 | | df-uni 3572 |
. 2
⊢ ∪ {x ∣ ∃y(x = ∪ y ∧ y ∈ A)} = {z ∣
∃v(z ∈ v ∧ v ∈ {x ∣
∃y(x = ∪ y ∧ y ∈ A)})} |
49 | 46, 47, 48 | 3eqtr4i 2067 |
1
⊢ ∪ ∪ A = ∪ {x ∣ ∃y(x = ∪ y ∧ y ∈ A)} |