Definition df-iun 4927

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 4964. Theorem uniiun 4989 provides a definition of ordinary union in terms of indexed union. Theorems fniunfv 7129 and funiunfv 7130 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 4925	. 2 class ∪ 𝑥 ∈ 𝐴 𝐵
5		vy	. . . . . 6 setvar 𝑦
6	5	cv 1538	. . . . 5 class 𝑦
7	6, 3	wcel 2107	. . . 4 wff 𝑦 ∈ 𝐵
8	7, 1, 2	wrex 3066	. . 3 wff ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵
9	8, 5	cab 2716	. 2 class {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵}
10	4, 9	wceq 1539	1 wff ∪ 𝑥 ∈ 𝐴 𝐵 = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵}

This definition is referenced by:  eliun  4929  iuneq12df  4951  nfiun  4955  nfiung  4957  nfiu1  4959  dfiun2g  4961  dfiunv2  4966  cbviun  4967  cbviung  4969  iunssf  4975  iunss  4976  uniiun  4989  iunsn  4996  iunopab  5473  iunopabOLD  5474  opeliunxp  5655  reliun  5728  fnasrn  7026  abrexex2g  7816  marypha2lem4  9206  cshwsiun  16810  cbviunf  30904  iuneq12daf  30905  iunrdx  30912  iunrnmptss  30914  bnj956  32765  bnj1143  32779  bnj1146  32780  bnj1400  32824  bnj882  32915  bnj18eq1  32916  bnj893  32917  bnj1398  33023  ralssiun  35587  volsupnfl  35831  ss2iundf  41274  opeliun2xp  45679  nfiund  46391  nfiundg  46392