Definition df-iun 4892

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 4928. Theorem uniiun 4953 provides a definition of ordinary union in terms of indexed union. Theorems fniunfv 7038 and funiunfv 7039 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

Step	Hyp	Ref	Expression
1		vx	. . 3 setvar 𝑥
2		cA	. . 3 class 𝐴
3		cB	. . 3 class 𝐵
4	1, 2, 3	ciun 4890	. 2 class ∪ 𝑥 ∈ 𝐴 𝐵
5		vy	. . . . . 6 setvar 𝑦
6	5	cv 1542	. . . . 5 class 𝑦
7	6, 3	wcel 2112	. . . 4 wff 𝑦 ∈ 𝐵
8	7, 1, 2	wrex 3052	. . 3 wff ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵
9	8, 5	cab 2714	. 2 class {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵}
10	4, 9	wceq 1543	1 wff ∪ 𝑥 ∈ 𝐴 𝐵 = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵}

This definition is referenced by:  eliun  4894  iuneq12df  4916  nfiun  4920  nfiung  4922  nfiu1  4924  dfiunv2  4930  cbviun  4931  cbviung  4933  iunssf  4939  iunss  4940  uniiun  4953  iunsn  4960  iunopab  5425  opeliunxp  5601  reliun  5671  fnasrn  6938  abrexex2g  7715  marypha2lem4  9032  cshwsiun  16616  cbviunf  30568  iuneq12daf  30569  iunrdx  30576  iunrnmptss  30578  bnj956  32423  bnj1143  32437  bnj1146  32438  bnj1400  32482  bnj882  32573  bnj18eq1  32574  bnj893  32575  bnj1398  32681  ralssiun  35264  volsupnfl  35508  ss2iundf  40885  opeliun2xp  45284  nfiund  45994  nfiundg  45995