Definition df-iun 3972

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 disjoint variable group (meaning 𝐴 cannot depend on 𝑥) and that 𝐵 and 𝑥 do not share a disjoint 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 4004. Theorem uniiun 4024 provides a definition of ordinary union in terms of indexed union. (Contributed by NM, 27-Jun-1998.)

Assertion

Ref	Expression
df-iun	⊢ ∪ 𝑥 ∈ 𝐴 𝐵 = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵}

Distinct variable groups:   𝑥,𝑦   𝑦,𝐴   𝑦,𝐵

Allowed substitution hints:   𝐴(𝑥)   𝐵(𝑥)

Detailed syntax breakdown of Definition df-iun

Step	Hyp	Ref	Expression
1		vx	. . 3 setvar 𝑥
2		cA	. . 3 class 𝐴
3		cB	. . 3 class 𝐵
4	1, 2, 3	ciun 3970	. 2 class ∪ 𝑥 ∈ 𝐴 𝐵
5		vy	. . . . . 6 setvar 𝑦
6	5	cv 1396	. . . . 5 class 𝑦
7	6, 3	wcel 2202	. . . 4 wff 𝑦 ∈ 𝐵
8	7, 1, 2	wrex 2511	. . 3 wff ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵
9	8, 5	cab 2217	. 2 class {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵}
10	4, 9	wceq 1397	1 wff ∪ 𝑥 ∈ 𝐴 𝐵 = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵}

This definition is referenced by:  eliun  3974  nfiunxy  3996  nfiunya  3998  nfiu1  4000  dfiunv2  4006  cbviun  4007  iunss  4011  uniiun  4024  iunopab  4376  opeliunxp  4781  reliun  4848  fnasrn  5825  fnasrng  5827  abrexex2g  6281  abrexex2  6285  bdciun  16473