Definition df-iun 4925

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 4963. Theorem uniiun 4990 provides a definition of ordinary union in terms of indexed union. Theorems fniunfv 7194 and funiunfv 7195 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 4923	. 2 class ∪ 𝑥 ∈ 𝐴 𝐵
5		vy	. . . . . 6 setvar 𝑦
6	5	cv 1547	. . . . 5 class 𝑦
7	6, 3	wcel 2121	. . . 4 wff 𝑦 ∈ 𝐵
8	7, 1, 2	wrex 3065	. . 3 wff ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵
9	8, 5	cab 2719	. 2 class {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵}
10	4, 9	wceq 1548	1 wff ∪ 𝑥 ∈ 𝐴 𝐵 = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵}

This definition is referenced by:  eliun  4927  iuneq12df  4950  iuneq12d  4953  nfiun  4955  nfiung  4957  dfiun2g  4961  dfiunv2  4965  cbviun  4966  cbviung  4968  cbviunv  4970  iunssfOLD  4975  iunssOLD  4977  uniiun  4990  iunid  4992  iunsn  4997  iunopab  5503  opeliunxp  5687  opeliun2xp  5688  fnasrn  7090  abrexex2g  7908  marypha2lem4  9345  cshwsiun  17065  cbviunf  32646  iuneq12daf  32647  iunrdx  32654  iunrnmptss  32656  bnj956  34972  bnj1143  34985  bnj1146  34986  bnj1400  35030  bnj882  35121  bnj18eq1  35122  bnj893  35123  bnj1398  35229  iuneq12i  36436  cbviunvw2  36473  cbviundavw  36503  cbviundavw2  36527  ralssiun  37782  volsupnfl  38045  iuneq1i  45545  nfiund  50176  nfiundg  50177