![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
Mirrors > Home > MPE Home > Th. List > xpiundir | Unicode version |
Description: Distributive law for Cartesian product over indexed union. (Contributed by Mario Carneiro, 27-Apr-2014.) |
Ref | Expression |
---|---|
xpiundir |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | rexcom4 3072 | . . . . 5 | |
2 | df-rex 2798 | . . . . . 6 | |
3 | 2 | rexbii 2813 | . . . . 5 |
4 | eliun 4257 | . . . . . . . 8 | |
5 | 4 | anbi1i 695 | . . . . . . 7 |
6 | r19.41v 2953 | . . . . . . 7 | |
7 | 5, 6 | bitr4i 252 | . . . . . 6 |
8 | 7 | exbii 1635 | . . . . 5 |
9 | 1, 3, 8 | 3bitr4ri 278 | . . . 4 |
10 | df-rex 2798 | . . . 4 | |
11 | elxp2 4940 | . . . . 5 | |
12 | 11 | rexbii 2813 | . . . 4 |
13 | 9, 10, 12 | 3bitr4i 277 | . . 3 |
14 | elxp2 4940 | . . 3 | |
15 | eliun 4257 | . . 3 | |
16 | 13, 14, 15 | 3bitr4i 277 | . 2 |
17 | 16 | eqriv 2446 | 1 |
Colors of variables: wff setvar class |
Syntax hints: /\ wa 369 = wceq 1370
E. wex 1587 e. wcel 1757 E. wrex 2793
<. cop 3965 U_ ciun 4253 X. cxp 4920 |
This theorem is referenced by: iunxpconst 4977 resiun2 5212 txbasval 19279 txtube 19313 txcmplem1 19314 ovoliunlem1 21085 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1592 ax-4 1603 ax-5 1671 ax-6 1709 ax-7 1729 ax-9 1761 ax-10 1776 ax-11 1781 ax-12 1793 ax-13 1944 ax-ext 2429 ax-sep 4495 ax-nul 4503 ax-pr 4613 |
This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3an 967 df-tru 1373 df-ex 1588 df-nf 1591 df-sb 1702 df-clab 2436 df-cleq 2442 df-clel 2445 df-nfc 2598 df-ne 2643 df-ral 2797 df-rex 2798 df-v 3054 df-dif 3413 df-un 3415 df-in 3417 df-ss 3424 df-nul 3720 df-if 3874 df-sn 3960 df-pr 3962 df-op 3966 df-iun 4255 df-opab 4433 df-xp 4928 |
Copyright terms: Public domain | W3C validator |