MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-iun Unicode version

Definition df-iun 4332
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 (x). We call the index, the index set, and the indexed set. In most books, is written as a subscript or underneath a union symbol U.. We use a special union symbol U_ 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 (x) i.e. can be substituted with a class expression containing ). An alternate definition tying indexed union to ordinary union is dfiun2 4364. Theorem uniiun 4383 provides a definition of ordinary union in terms of indexed union. Theorems fniunfv 6159 and funiunfv 6160 are useful when is a function. (Contributed by NM, 27-Jun-1998.)
Assertion
Ref Expression
df-iun
Distinct variable groups:   ,   ,   ,

Detailed syntax breakdown of Definition df-iun
StepHypRef Expression
1 vx . . 3
2 cA . . 3
3 cB . . 3
41, 2, 3ciun 4330 . 2
5 vy . . . . . 6
65cv 1394 . . . . 5
76, 3wcel 1818 . . . 4
87, 1, 2wrex 2808 . . 3
98, 5cab 2442 . 2
104, 9wceq 1395 1
Colors of variables: wff setvar class
This definition is referenced by:  rabasiun  4334  eliun  4335  iuneq12df  4354  nfiun  4358  nfiu1  4360  dfiunv2  4366  cbviun  4367  iunss  4371  uniiun  4383  iunopab  4788  opeliunxp  5056  reliun  5128  fnasrn  6077  abrexex2g  6777  abrexex2  6781  marypha2lem4  7918  cshwsiun  14584  iuneq12daf  27425  iunrdx  27431  volsupnfl  30059  opeliun2xp  32922  bnj956  33835  bnj1143  33849  bnj1146  33850  bnj1400  33894  bnj882  33984  bnj18eq1  33985  bnj893  33986  bnj1398  34090
  Copyright terms: Public domain W3C validator