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 4914
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 4950. Theorem uniiun 4974 provides a definition of ordinary union in terms of indexed union. Theorems fniunfv 6997 and funiunfv 6998 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 4912 . 2 class 𝑥𝐴 𝐵
5 vy . . . . . 6 setvar 𝑦
65cv 1527 . . . . 5 class 𝑦
76, 3wcel 2105 . . . 4 wff 𝑦𝐵
87, 1, 2wrex 3139 . . 3 wff 𝑥𝐴 𝑦𝐵
98, 5cab 2799 . 2 class {𝑦 ∣ ∃𝑥𝐴 𝑦𝐵}
104, 9wceq 1528 1 wff 𝑥𝐴 𝐵 = {𝑦 ∣ ∃𝑥𝐴 𝑦𝐵}
Colors of variables: wff setvar class
This definition is referenced by:  eliun  4916  iuneq12df  4937  nfiun  4941  nfiung  4943  nfiu1  4945  dfiunv2  4952  cbviun  4953  cbviung  4955  iunss  4961  uniiun  4974  iunopab  5438  opeliunxp  5613  reliun  5683  fnasrn  6900  abrexex2g  7656  marypha2lem4  8891  cshwsiun  16423  cbviunf  30236  iuneq12daf  30237  iunrdx  30244  iunrnmptss  30246  bnj956  31948  bnj1143  31962  bnj1146  31963  bnj1400  32007  bnj882  32098  bnj18eq1  32099  bnj893  32100  bnj1398  32204  ralssiun  34571  volsupnfl  34819  iunsn  38998  ss2iundf  39884  iunssf  41232  opeliun2xp  44279  nfiund  44675  nfiundg  44676
  Copyright terms: Public domain W3C validator