Definition df-iun 4956

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 4994. Theorem uniiun 5021 provides a definition of ordinary union in terms of indexed union. Theorems fniunfv 7247 and funiunfv 7248 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 4954	. 2 class ∪ 𝑥 ∈ 𝐴 𝐵
5		vy	. . . . . 6 setvar 𝑦
6	5	cv 1569	. . . . 5 class 𝑦
7	6, 3	wcel 2145	. . . 4 wff 𝑦 ∈ 𝐵
8	7, 1, 2	wrex 3088	. . 3 wff ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵
9	8, 5	cab 2740	. 2 class {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵}
10	4, 9	wceq 1570	1 wff ∪ 𝑥 ∈ 𝐴 𝐵 = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵}

This definition is used by:  eliun  4958  iuneq12df  4981  iuneq12d  4984  nfiun  4986  nfiung  4988  dfiun2g  4992  dfiunv2  4996  cbviun  4997  cbviung  4999  cbviunv  5001  iunssfOLD  5006  iunssOLD  5008  uniiun  5021  iunid  5023  iunsn  5028  iunopab  5542  opeliunxp  5726  opeliun2xp  5727  fnasrn  7144  abrexex2g  7964  marypha2lem4  9411  cshwsiun  17195  cbviunf  33015  iuneq12daf  33016  iunrdx  33023  iunrnmptss  33025  bnj956  35273  bnj1143  35286  bnj1146  35287  bnj1400  35331  bnj882  35422  bnj18eq1  35423  bnj893  35424  bnj1398  35530  iuneq12i  36802  cbviunvw2  36839  cbviundavw  36869  cbviundavw2  36893  ralssiun  38148  volsupnfl  38401  iuneq1i  45905  nfiund  50587  nfiundg  50588