| Metamath Proof Explorer |
< Previous
Next >
Related theorems Unicode version |
| Description: Distributive law for cross product over union. Theorem 103 of [Suppes] p. 52. |
| Ref | Expression |
|---|---|
| xpundi |
|
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | elun 2169 |
. . . . . 6
| |
| 2 | 1 | anbi2i 480 |
. . . . 5
|
| 3 | andi 603 |
. . . . 5
| |
| 4 | 2, 3 | bitr 173 |
. . . 4
|
| 5 | 4 | opabbii 2666 |
. . 3
|
| 6 | unopab 2674 |
. . 3
| |
| 7 | 5, 6 | eqtr4 1495 |
. 2
|
| 8 | df-xp 3179 |
. 2
| |
| 9 | df-xp 3179 |
. . 3
| |
| 10 | df-xp 3179 |
. . 3
| |
| 11 | 9, 10 | uneq12i 2178 |
. 2
|
| 12 | 7, 8, 11 | 3eqtr4 1502 |
1
|
| Colors of variables: wff set class |
| Syntax hints: |
| This theorem is referenced by: xpun 3222 xp2cda 4908 xpcdaen 4911 alephadd 7532 |
| This theorem was proved from axioms: ax-1 4 ax-2 5 ax-3 6 ax-mp 7 ax-7 960 ax-gen 961 ax-8 962 ax-10 964 ax-12 966 ax-17 969 ax-4 971 ax-5o 973 ax-6o 976 ax-9o 1121 ax-10o 1138 ax-16 1208 ax-11o 1216 ax-ext 1457 |
| This theorem depends on definitions: df-bi 147 df-or 224 df-an 225 df-ex 979 df-sb 1170 df-clab 1462 df-cleq 1467 df-clel 1470 df-v 1808 df-un 2046 df-opab 2662 df-xp 3179 |