Definition df-iun 4950

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 4989. Theorem uniiun 5016 provides a definition of ordinary union in terms of indexed union. Theorems fniunfv 7205 and funiunfv 7206 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 4948	. 2 class ∪ 𝑥 ∈ 𝐴 𝐵
5		vy	. . . . . 6 setvar 𝑦
6	5	cv 1541	. . . . 5 class 𝑦
7	6, 3	wcel 2114	. . . 4 wff 𝑦 ∈ 𝐵
8	7, 1, 2	wrex 3062	. . 3 wff ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵
9	8, 5	cab 2715	. 2 class {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵}
10	4, 9	wceq 1542	1 wff ∪ 𝑥 ∈ 𝐴 𝐵 = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵}

This definition is referenced by:  eliun  4952  iuneq12df  4975  iuneq12d  4978  nfiun  4980  nfiung  4982  nfiu1OLD  4985  dfiun2g  4987  dfiunv2  4991  cbviun  4992  cbviung  4994  cbviunv  4996  iunssfOLD  5001  iunssOLD  5003  uniiun  5016  iunid  5018  iunsn  5023  iunopab  5517  opeliunxp  5701  opeliun2xp  5702  fnasrn  7102  abrexex2g  7920  marypha2lem4  9355  cshwsiun  17041  cbviunf  32648  iuneq12daf  32649  iunrdx  32656  iunrnmptss  32658  bnj956  34959  bnj1143  34972  bnj1146  34973  bnj1400  35017  bnj882  35108  bnj18eq1  35109  bnj893  35110  bnj1398  35216  iuneq12i  36417  cbviunvw2  36454  cbviundavw  36484  cbviundavw2  36508  ralssiun  37689  volsupnfl  37945  iuneq1i  45473  nfiund  50062  nfiundg  50063