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 4999
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 5037. Theorem uniiun 5062 provides a definition of ordinary union in terms of indexed union. Theorems fniunfv 7257 and funiunfv 7258 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 4997 . 2 class 𝑥𝐴 𝐵
5 vy . . . . . 6 setvar 𝑦
65cv 1532 . . . . 5 class 𝑦
76, 3wcel 2098 . . . 4 wff 𝑦𝐵
87, 1, 2wrex 3059 . . 3 wff 𝑥𝐴 𝑦𝐵
98, 5cab 2702 . 2 class {𝑦 ∣ ∃𝑥𝐴 𝑦𝐵}
104, 9wceq 1533 1 wff 𝑥𝐴 𝐵 = {𝑦 ∣ ∃𝑥𝐴 𝑦𝐵}
Colors of variables: wff setvar class
This definition is referenced by:  eliun  5001  iuneq12df  5023  nfiun  5027  nfiung  5029  nfiu1OLD  5032  dfiun2g  5034  dfiunv2  5039  cbviun  5040  cbviung  5042  iunssf  5048  iunss  5049  uniiun  5062  iunid  5064  iunsn  5070  iunopab  5561  iunopabOLD  5562  opeliunxp  5745  reliun  5818  fnasrn  7154  abrexex2g  7969  marypha2lem4  9463  cshwsiun  17072  cbviunf  32425  iuneq12daf  32426  iunrdx  32433  iunrnmptss  32435  bnj956  34535  bnj1143  34549  bnj1146  34550  bnj1400  34594  bnj882  34685  bnj18eq1  34686  bnj893  34687  bnj1398  34793  ralssiun  37014  volsupnfl  37266  opeliun2xp  47579  nfiund  48288  nfiundg  48289
  Copyright terms: Public domain W3C validator