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

Definition df-iun 4886
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 4923. Theorem uniiun 4948 provides a definition of ordinary union in terms of indexed union. Theorems fniunfv 6988 and funiunfv 6989 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 setvar 𝑥
2 cA . . 3 class 𝐴
3 cB . . 3 class 𝐵
41, 2, 3ciun 4884 . 2 class 𝑥𝐴 𝐵
5 vy . . . . . 6 setvar 𝑦
65cv 1537 . . . . 5 class 𝑦
76, 3wcel 2112 . . . 4 wff 𝑦𝐵
87, 1, 2wrex 3110 . . 3 wff 𝑥𝐴 𝑦𝐵
98, 5cab 2779 . 2 class {𝑦 ∣ ∃𝑥𝐴 𝑦𝐵}
104, 9wceq 1538 1 wff 𝑥𝐴 𝐵 = {𝑦 ∣ ∃𝑥𝐴 𝑦𝐵}
Colors of variables: wff setvar class
This definition is referenced by:  eliun  4888  iuneq12df  4910  nfiun  4914  nfiung  4916  nfiu1  4918  dfiunv2  4925  cbviun  4926  cbviung  4928  iunssf  4934  iunss  4935  uniiun  4948  iunopab  5414  opeliunxp  5587  reliun  5657  fnasrn  6888  abrexex2g  7651  marypha2lem4  8890  cshwsiun  16429  cbviunf  30323  iuneq12daf  30324  iunrdx  30331  iunrnmptss  30333  bnj956  32162  bnj1143  32176  bnj1146  32177  bnj1400  32221  bnj882  32312  bnj18eq1  32313  bnj893  32314  bnj1398  32420  ralssiun  34825  volsupnfl  35101  iunsn  39405  ss2iundf  40353  opeliun2xp  44727  nfiund  45197  nfiundg  45198
  Copyright terms: Public domain W3C validator