Metamath Proof Explorer


Theorem uniuni

Description: Expression for double union that moves union into a class abstraction. (Contributed by FL, 28-May-2007)

Ref Expression
Assertion uniuni A=x|yx=yyA

Proof

Step Hyp Ref Expression
1 eluni uAyuyyA
2 1 anbi2i zuuAzuyuyyA
3 2 exbii uzuuAuzuyuyyA
4 19.42v yzuuyyAzuyuyyA
5 4 bicomi zuyuyyAyzuuyyA
6 5 exbii uzuyuyyAuyzuuyyA
7 excom uyzuuyyAyuzuuyyA
8 anass zuuyyAzuuyyA
9 ancom zuuyyAyAzuuy
10 8 9 bitr3i zuuyyAyAzuuy
11 10 2exbii yuzuuyyAyuyAzuuy
12 exdistr yuyAzuuyyyAuzuuy
13 7 11 12 3bitri uyzuuyyAyyAuzuuy
14 eluni zyuzuuy
15 14 bicomi uzuuyzy
16 15 anbi2i yAuzuuyyAzy
17 16 exbii yyAuzuuyyyAzy
18 6 13 17 3bitri uzuyuyyAyyAzy
19 vuniex yV
20 eleq2 v=yzvzy
21 19 20 ceqsexv vv=yzvzy
22 exancom vv=yzvvzvv=y
23 21 22 bitr3i zyvzvv=y
24 23 anbi2i yAzyyAvzvv=y
25 19.42v vyAzvv=yyAvzvv=y
26 ancom yAzvv=yzvv=yyA
27 anass zvv=yyAzvv=yyA
28 26 27 bitri yAzvv=yzvv=yyA
29 28 exbii vyAzvv=yvzvv=yyA
30 24 25 29 3bitr2i yAzyvzvv=yyA
31 30 exbii yyAzyyvzvv=yyA
32 excom yvzvv=yyAvyzvv=yyA
33 exdistr vyzvv=yyAvzvyv=yyA
34 vex vV
35 eqeq1 x=vx=yv=y
36 35 anbi1d x=vx=yyAv=yyA
37 36 exbidv x=vyx=yyAyv=yyA
38 34 37 elab vx|yx=yyAyv=yyA
39 38 bicomi yv=yyAvx|yx=yyA
40 39 anbi2i zvyv=yyAzvvx|yx=yyA
41 40 exbii vzvyv=yyAvzvvx|yx=yyA
42 33 41 bitri vyzvv=yyAvzvvx|yx=yyA
43 31 32 42 3bitri yyAzyvzvvx|yx=yyA
44 3 18 43 3bitri uzuuAvzvvx|yx=yyA
45 44 abbii z|uzuuA=z|vzvvx|yx=yyA
46 df-uni A=z|uzuuA
47 df-uni x|yx=yyA=z|vzvvx|yx=yyA
48 45 46 47 3eqtr4i A=x|yx=yyA