Definition df-iun 4957

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 4995. Theorem uniiun 5022 provides a definition of ordinary union in terms of indexed union. Theorems fniunfv 7245 and funiunfv 7246 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 4955	. 2 class ∪ 𝑥 ∈ 𝐴 𝐵
5		vy	. . . . . 6 setvar 𝑦
6	5	cv 1567	. . . . 5 class 𝑦
7	6, 3	wcel 2141	. . . 4 wff 𝑦 ∈ 𝐵
8	7, 1, 2	wrex 3087	. . 3 wff ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵
9	8, 5	cab 2739	. 2 class {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵}
10	4, 9	wceq 1568	1 wff ∪ 𝑥 ∈ 𝐴 𝐵 = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵}

This definition is referenced by:  eliun  4959  iuneq12df  4982  iuneq12d  4985  nfiun  4987  nfiung  4989  dfiun2g  4993  dfiunv2  4997  cbviun  4998  cbviung  5000  cbviunv  5002  iunssfOLD  5007  iunssOLD  5009  uniiun  5022  iunid  5024  iunsn  5029  iunopab  5544  opeliunxp  5728  opeliun2xp  5729  fnasrn  7141  abrexex2g  7960  marypha2lem4  9397  cshwsiun  17158  cbviunf  32866  iuneq12daf  32867  iunrdx  32874  iunrnmptss  32876  bnj956  35131  bnj1143  35144  bnj1146  35145  bnj1400  35189  bnj882  35280  bnj18eq1  35281  bnj893  35282  bnj1398  35388  iuneq12i  36651  cbviunvw2  36688  cbviundavw  36718  cbviundavw2  36742  ralssiun  37997  volsupnfl  38260  iuneq1i  45752  nfiund  50397  nfiundg  50398