NFE Home New Foundations Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  df-iun GIF version

Definition df-iun 3971
Description: Define indexed union. Definition indexed union in [Stoll] p. 45. In most applications, A is independent of x (although this is not required by the definition), and B depends on x i.e. can be read informally as B(x). We call x the index, A the index set, and B the indexed set. In most books, x A 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 x and A are in the same distinct variable group (meaning A cannot depend on x) and that B and x do not share a distinct variable group (meaning that can be thought of as B(x) i.e. can be substituted with a class expression containing x). An alternate definition tying indexed union to ordinary union is dfiun2 4001. Theorem uniiun 4019 provides a definition of ordinary union in terms of indexed union. Theorems fniunfv 5466 and funiunfv 5467 are useful when B is a function. (Contributed by NM, 27-Jun-1998.)
Ref Expression
df-iun x A B = {y x A y B}
Distinct variable groups:   x,y   y,A   y,B
Allowed substitution hints:   A(x)   B(x)

Detailed syntax breakdown of Definition df-iun
StepHypRef Expression
1 vx . . 3 setvar x
2 cA . . 3 class A
3 cB . . 3 class B
41, 2, 3ciun 3969 . 2 class x A B
5 vy . . . . . 6 setvar y
65cv 1641 . . . . 5 class y
76, 3wcel 1710 . . . 4 wff y B
87, 1, 2wrex 2615 . . 3 wff x A y B
98, 5cab 2339 . 2 class {y x A y B}
104, 9wceq 1642 1 wff x A B = {y x A y B}
Colors of variables: wff setvar class
This definition is referenced by:  eliun  3973  nfiun  3995  nfiu1  3997  cbviun  4003  iunss  4007  uniiun  4019  opeliunxp  4820  iunfopab  5204
  Copyright terms: Public domain W3C validator