Definition df-iun 4952

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 7251 and funiunfv 7252 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 4950	. 2 class ∪ 𝑥 ∈ 𝐴 𝐵
5		vy	. . . . . 6 setvar 𝑦
6	5	cv 1568	. . . . 5 class 𝑦
7	6, 3	wcel 2144	. . . 4 wff 𝑦 ∈ 𝐵
8	7, 1, 2	wrex 3086	. . 3 wff ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵
9	8, 5	cab 2738	. 2 class {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵}
10	4, 9	wceq 1569	1 wff ∪ 𝑥 ∈ 𝐴 𝐵 = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵}

This definition is used by:  eliun  4954  iuneq12df  4977  iuneq12d  4979  nfiun  4981  nfiung  4983  dfiun2g  4987  dfiunv2  4991  cbviun  4992  cbviung  4994  cbviunv  4996  iunssfOLD  5001  iunssOLD  5003  uniiun  5016  iunid  5018  iunsn  5023  iunopab  5533  opeliunxp  5717  opeliun2xp  5718  fnasrn  7148  abrexex2g  7976  marypha2lem4  9430  cshwsiun  17277  cbviunf  33192  iuneq12daf  33193  iunrdx  33200  iunrnmptss  33201  bnj956  35449  bnj1143  35462  bnj1146  35463  bnj1400  35507  bnj882  35598  bnj18eq1  35599  bnj893  35600  bnj1398  35706  iuneq12i  37026  cbviunvw2  37063  cbviundavw  37093  cbviundavw2  37117  ralssiun  38373  volsupnfl  38626  dfproplem  38684  iuneq1i  46143  nfiund  50824  nfiundg  50825