Definition df-iun 4957

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

This definition is used by:  eliun  4959  iuneq12df  4982  iuneq12d  4985  nfiun  4987  nfiung  4989  dfiun2g  4993  dfiunv2  4997  cbviun  4998  cbviung  5000  cbviunv  5002  iunssfOLD  5007  iunssOLD  5009  uniiun  5022  iunid  5024  iunsn  5029  iunopab  5543  opeliunxp  5727  opeliun2xp  5728  fnasrn  7141  abrexex2g  7959  marypha2lem4  9396  cshwsiun  17165  cbviunf  32911  iuneq12daf  32912  iunrdx  32919  iunrnmptss  32921  bnj956  35174  bnj1143  35187  bnj1146  35188  bnj1400  35232  bnj882  35323  bnj18eq1  35324  bnj893  35325  bnj1398  35431  iuneq12i  36735  cbviunvw2  36772  cbviundavw  36802  cbviundavw2  36826  ralssiun  38081  volsupnfl  38344  iuneq1i  45832  nfiund  50480  nfiundg  50481