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 | y x = y y A

Proof

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