Description: Distributive law for Cartesian product over indexed union. (Contributed by Mario Carneiro, 27-Apr-2014)
Ref | Expression | ||
---|---|---|---|
Assertion | xpiundir | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | rexcom4 | |
|
2 | df-rex | |
|
3 | 2 | rexbii | |
4 | eliun | |
|
5 | 4 | anbi1i | |
6 | r19.41v | |
|
7 | 5 6 | bitr4i | |
8 | 7 | exbii | |
9 | 1 3 8 | 3bitr4ri | |
10 | df-rex | |
|
11 | elxp2 | |
|
12 | 11 | rexbii | |
13 | 9 10 12 | 3bitr4i | |
14 | elxp2 | |
|
15 | eliun | |
|
16 | 13 14 15 | 3bitr4i | |
17 | 16 | eqriv | |