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

Definition df-iun 4174
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 4205. Theorem uniiun 4224 provides a definition of ordinary union in terms of indexed union. Theorems fniunfv 6094 and funiunfv 6095 are useful when 𝐵 is a function. (Contributed by NM, 27-Jun-1998.)
Assertion
Ref Expression
df-iun 𝑥𝐴 𝐵 = {𝑦 ∣ ∃𝑥𝐴 𝑦𝐵}
Distinct variable groups:   𝑥,𝑦   𝑦,𝐴   𝑦,𝐵
Allowed substitution hints:   𝐴(𝑥)   𝐵(𝑥)

Detailed syntax breakdown of Definition df-iun
StepHypRef Expression
1 vx . . 3 set 𝑥
2 cA . . 3 class 𝐴
3 cB . . 3 class 𝐵
41, 2, 3ciun 4172 . 2 class 𝑥𝐴 𝐵
5 vy . . . . . 6 set 𝑦
65cv 1661 . . . . 5 class 𝑦
76, 3wcel 1734 . . . 4 wff 𝑦𝐵
87, 1, 2wrex 2749 . . 3 wff 𝑥𝐴 𝑦𝐵
98, 5cab 2465 . 2 class {𝑦 ∣ ∃𝑥𝐴 𝑦𝐵}
104, 9wceq 1662 1 wff 𝑥𝐴 𝐵 = {𝑦 ∣ ∃𝑥𝐴 𝑦𝐵}
Colors of variables: wff set class
This definition is referenced by:  eliun  4176  iuneq12df  4195  nfiun  4199  nfiu1  4201  dfiunv2  4207  cbviun  4208  iunss  4212  uniiun  4224  iunopab  4578  opeliunxp  5020  reliun  5088  fnasrn  6012  abrexex2g  6088  abrexex2  6101  marypha2lem4  7538  iuneq12daf  24148  iunrdx  24154  volsupnfl  26705  rabasiun  28760  cshwsiun  28951  bnj956  30115  bnj1143  30129  bnj1146  30130  bnj1400  30175  bnj882  30265  bnj18eq1  30266  bnj893  30267  bnj1398  30371
  Copyright terms: Public domain W3C validator