Definition df-iun

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 e. A is written as a subscript or underneath a union symbol U. . We use a special union symbol U_ 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 . Theorem uniiun provides a definition of ordinary union in terms of indexed union. Theorems fniunfv and funiunfv are useful when B is a function. (Contributed by NM, 27-Jun-1998)

	Ref	Expression
Assertion	df-iun	$$⊢\bigcup _{x\in A}B=\left\{y|\exists x\in Ay\in B\right\}$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		vx	$$setvarx$$
1		cA	$$classA$$
2		cB	$$classB$$
3	0 1 2	ciun	$$class\bigcup _{x\in A}B$$
4		vy	$$setvary$$
5	4	cv	$$setvary$$
6	5 2	wcel	$$wffy\in B$$
7	6 0 1	wrex	$$wff\exists x\in Ay\in B$$
8	7 4	cab	$$class\left\{y|\exists x\in Ay\in B\right\}$$
9	3 8	wceq	$$wff\bigcup _{x\in A}B=\left\{y|\exists x\in Ay\in B\right\}$$