Step |
Hyp |
Ref |
Expression |
1 |
|
eluni |
|- ( u e. U. A <-> E. y ( u e. y /\ y e. A ) ) |
2 |
1
|
anbi2i |
|- ( ( z e. u /\ u e. U. A ) <-> ( z e. u /\ E. y ( u e. y /\ y e. A ) ) ) |
3 |
2
|
exbii |
|- ( E. u ( z e. u /\ u e. U. A ) <-> E. u ( z e. u /\ E. y ( u e. y /\ y e. A ) ) ) |
4 |
|
19.42v |
|- ( E. y ( z e. u /\ ( u e. y /\ y e. A ) ) <-> ( z e. u /\ E. y ( u e. y /\ y e. A ) ) ) |
5 |
4
|
bicomi |
|- ( ( z e. u /\ E. y ( u e. y /\ y e. A ) ) <-> E. y ( z e. u /\ ( u e. y /\ y e. A ) ) ) |
6 |
5
|
exbii |
|- ( E. u ( z e. u /\ E. y ( u e. y /\ y e. A ) ) <-> E. u E. y ( z e. u /\ ( u e. y /\ y e. A ) ) ) |
7 |
|
excom |
|- ( E. u E. y ( z e. u /\ ( u e. y /\ y e. A ) ) <-> E. y E. u ( z e. u /\ ( u e. y /\ y e. A ) ) ) |
8 |
|
anass |
|- ( ( ( z e. u /\ u e. y ) /\ y e. A ) <-> ( z e. u /\ ( u e. y /\ y e. A ) ) ) |
9 |
|
ancom |
|- ( ( ( z e. u /\ u e. y ) /\ y e. A ) <-> ( y e. A /\ ( z e. u /\ u e. y ) ) ) |
10 |
8 9
|
bitr3i |
|- ( ( z e. u /\ ( u e. y /\ y e. A ) ) <-> ( y e. A /\ ( z e. u /\ u e. y ) ) ) |
11 |
10
|
2exbii |
|- ( E. y E. u ( z e. u /\ ( u e. y /\ y e. A ) ) <-> E. y E. u ( y e. A /\ ( z e. u /\ u e. y ) ) ) |
12 |
|
exdistr |
|- ( E. y E. u ( y e. A /\ ( z e. u /\ u e. y ) ) <-> E. y ( y e. A /\ E. u ( z e. u /\ u e. y ) ) ) |
13 |
7 11 12
|
3bitri |
|- ( E. u E. y ( z e. u /\ ( u e. y /\ y e. A ) ) <-> E. y ( y e. A /\ E. u ( z e. u /\ u e. y ) ) ) |
14 |
|
eluni |
|- ( z e. U. y <-> E. u ( z e. u /\ u e. y ) ) |
15 |
14
|
bicomi |
|- ( E. u ( z e. u /\ u e. y ) <-> z e. U. y ) |
16 |
15
|
anbi2i |
|- ( ( y e. A /\ E. u ( z e. u /\ u e. y ) ) <-> ( y e. A /\ z e. U. y ) ) |
17 |
16
|
exbii |
|- ( E. y ( y e. A /\ E. u ( z e. u /\ u e. y ) ) <-> E. y ( y e. A /\ z e. U. y ) ) |
18 |
6 13 17
|
3bitri |
|- ( E. u ( z e. u /\ E. y ( u e. y /\ y e. A ) ) <-> E. y ( y e. A /\ z e. U. y ) ) |
19 |
|
vuniex |
|- U. y e. _V |
20 |
|
eleq2 |
|- ( v = U. y -> ( z e. v <-> z e. U. y ) ) |
21 |
19 20
|
ceqsexv |
|- ( E. v ( v = U. y /\ z e. v ) <-> z e. U. y ) |
22 |
|
exancom |
|- ( E. v ( v = U. y /\ z e. v ) <-> E. v ( z e. v /\ v = U. y ) ) |
23 |
21 22
|
bitr3i |
|- ( z e. U. y <-> E. v ( z e. v /\ v = U. y ) ) |
24 |
23
|
anbi2i |
|- ( ( y e. A /\ z e. U. y ) <-> ( y e. A /\ E. v ( z e. v /\ v = U. y ) ) ) |
25 |
|
19.42v |
|- ( E. v ( y e. A /\ ( z e. v /\ v = U. y ) ) <-> ( y e. A /\ E. v ( z e. v /\ v = U. y ) ) ) |
26 |
|
ancom |
|- ( ( y e. A /\ ( z e. v /\ v = U. y ) ) <-> ( ( z e. v /\ v = U. y ) /\ y e. A ) ) |
27 |
|
anass |
|- ( ( ( z e. v /\ v = U. y ) /\ y e. A ) <-> ( z e. v /\ ( v = U. y /\ y e. A ) ) ) |
28 |
26 27
|
bitri |
|- ( ( y e. A /\ ( z e. v /\ v = U. y ) ) <-> ( z e. v /\ ( v = U. y /\ y e. A ) ) ) |
29 |
28
|
exbii |
|- ( E. v ( y e. A /\ ( z e. v /\ v = U. y ) ) <-> E. v ( z e. v /\ ( v = U. y /\ y e. A ) ) ) |
30 |
24 25 29
|
3bitr2i |
|- ( ( y e. A /\ z e. U. y ) <-> E. v ( z e. v /\ ( v = U. y /\ y e. A ) ) ) |
31 |
30
|
exbii |
|- ( E. y ( y e. A /\ z e. U. y ) <-> E. y E. v ( z e. v /\ ( v = U. y /\ y e. A ) ) ) |
32 |
|
excom |
|- ( E. y E. v ( z e. v /\ ( v = U. y /\ y e. A ) ) <-> E. v E. y ( z e. v /\ ( v = U. y /\ y e. A ) ) ) |
33 |
|
exdistr |
|- ( E. v E. y ( z e. v /\ ( v = U. y /\ y e. A ) ) <-> E. v ( z e. v /\ E. y ( v = U. y /\ y e. A ) ) ) |
34 |
|
vex |
|- v e. _V |
35 |
|
eqeq1 |
|- ( x = v -> ( x = U. y <-> v = U. y ) ) |
36 |
35
|
anbi1d |
|- ( x = v -> ( ( x = U. y /\ y e. A ) <-> ( v = U. y /\ y e. A ) ) ) |
37 |
36
|
exbidv |
|- ( x = v -> ( E. y ( x = U. y /\ y e. A ) <-> E. y ( v = U. y /\ y e. A ) ) ) |
38 |
34 37
|
elab |
|- ( v e. { x | E. y ( x = U. y /\ y e. A ) } <-> E. y ( v = U. y /\ y e. A ) ) |
39 |
38
|
bicomi |
|- ( E. y ( v = U. y /\ y e. A ) <-> v e. { x | E. y ( x = U. y /\ y e. A ) } ) |
40 |
39
|
anbi2i |
|- ( ( z e. v /\ E. y ( v = U. y /\ y e. A ) ) <-> ( z e. v /\ v e. { x | E. y ( x = U. y /\ y e. A ) } ) ) |
41 |
40
|
exbii |
|- ( E. v ( z e. v /\ E. y ( v = U. y /\ y e. A ) ) <-> E. v ( z e. v /\ v e. { x | E. y ( x = U. y /\ y e. A ) } ) ) |
42 |
33 41
|
bitri |
|- ( E. v E. y ( z e. v /\ ( v = U. y /\ y e. A ) ) <-> E. v ( z e. v /\ v e. { x | E. y ( x = U. y /\ y e. A ) } ) ) |
43 |
31 32 42
|
3bitri |
|- ( E. y ( y e. A /\ z e. U. y ) <-> E. v ( z e. v /\ v e. { x | E. y ( x = U. y /\ y e. A ) } ) ) |
44 |
3 18 43
|
3bitri |
|- ( E. u ( z e. u /\ u e. U. A ) <-> E. v ( z e. v /\ v e. { x | E. y ( x = U. y /\ y e. A ) } ) ) |
45 |
44
|
abbii |
|- { z | E. u ( z e. u /\ u e. U. A ) } = { z | E. v ( z e. v /\ v e. { x | E. y ( x = U. y /\ y e. A ) } ) } |
46 |
|
df-uni |
|- U. U. A = { z | E. u ( z e. u /\ u e. U. A ) } |
47 |
|
df-uni |
|- U. { x | E. y ( x = U. y /\ y e. A ) } = { z | E. v ( z e. v /\ v e. { x | E. y ( x = U. y /\ y e. A ) } ) } |
48 |
45 46 47
|
3eqtr4i |
|- U. U. A = U. { x | E. y ( x = U. y /\ y e. A ) } |