Definition df-iun 4997

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 5037. Theorem uniiun 5062 provides a definition of ordinary union in terms of indexed union. Theorems fniunfv 7266 and funiunfv 7267 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 4995	. 2 class ∪ 𝑥 ∈ 𝐴 𝐵
5		vy	. . . . . 6 setvar 𝑦
6	5	cv 1535	. . . . 5 class 𝑦
7	6, 3	wcel 2105	. . . 4 wff 𝑦 ∈ 𝐵
8	7, 1, 2	wrex 3067	. . 3 wff ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵
9	8, 5	cab 2711	. 2 class {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵}
10	4, 9	wceq 1536	1 wff ∪ 𝑥 ∈ 𝐴 𝐵 = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵}

This definition is referenced by:  eliun  4999  iuneq12df  5022  iuneq12d  5025  nfiun  5027  nfiung  5029  nfiu1OLD  5032  dfiun2g  5034  dfiunv2  5039  cbviun  5040  cbviung  5042  cbviunv  5044  iunssf  5048  iunss  5049  uniiun  5062  iunid  5064  iunsn  5070  iunopab  5568  iunopabOLD  5569  opeliunxp  5755  reliun  5828  fnasrn  7164  abrexex2g  7987  marypha2lem4  9475  cshwsiun  17133  cbviunf  32575  iuneq12daf  32576  iunrdx  32583  iunrnmptss  32585  bnj956  34768  bnj1143  34782  bnj1146  34783  bnj1400  34827  bnj882  34918  bnj18eq1  34919  bnj893  34920  bnj1398  35026  iuneq12i  36176  cbviunvw2  36214  cbviundavw  36244  cbviundavw2  36268  ralssiun  37389  volsupnfl  37651  iuneq1i  45024  opeliun2xp  48177  nfiund  48904  nfiundg  48905