Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > df-iun | Structured version Visualization version Unicode version |
Description: Define indexed union. Definition indexed union in [Stoll] p. 45. In most applications, is independent of (although this is not required by the definition), and depends on i.e. can be read informally as . We call the index, the index set, and the indexed set. In most books, is written as a subscript or underneath a union symbol . We use a special union symbol to make it easier to distinguish from plain class union. In many theorems, you will see that and are in the same distinct variable group (meaning cannot depend on ) and that and do not share a distinct variable group (meaning that can be thought of as i.e. can be substituted with a class expression containing ). An alternate definition tying indexed union to ordinary union is dfiun2 4554. Theorem uniiun 4573 provides a definition of ordinary union in terms of indexed union. Theorems fniunfv 6505 and funiunfv 6506 are useful when is a function. (Contributed by NM, 27-Jun-1998.) |
Ref | Expression |
---|---|
df-iun |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | vx | . . 3 | |
2 | cA | . . 3 | |
3 | cB | . . 3 | |
4 | 1, 2, 3 | ciun 4520 | . 2 |
5 | vy | . . . . . 6 | |
6 | 5 | cv 1482 | . . . . 5 |
7 | 6, 3 | wcel 1990 | . . . 4 |
8 | 7, 1, 2 | wrex 2913 | . . 3 |
9 | 8, 5 | cab 2608 | . 2 |
10 | 4, 9 | wceq 1483 | 1 |
Colors of variables: wff setvar class |
This definition is referenced by: eliun 4524 iuneq12df 4544 nfiun 4548 nfiu1 4550 dfiunv2 4556 cbviun 4557 iunss 4561 uniiun 4573 iunopab 5012 opeliunxp 5170 reliun 5239 fnasrn 6411 abrexex2g 7144 abrexex2OLD 7150 marypha2lem4 8344 cshwsiun 15806 cbviunf 29372 iuneq12daf 29373 iunrdx 29382 bnj956 30847 bnj1143 30861 bnj1146 30862 bnj1400 30906 bnj882 30996 bnj18eq1 30997 bnj893 30998 bnj1398 31102 volsupnfl 33454 ss2iundf 37951 iunssf 39263 opeliun2xp 42111 nfiund 42421 |
Copyright terms: Public domain | W3C validator |