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 7191 and funiunfv 7192 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 1541	. . . . 5 class 𝑦
7	6, 3	wcel 2114	. . . 4 wff 𝑦 ∈ 𝐵
8	7, 1, 2	wrex 3059	. . 3 wff ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵
9	8, 5	cab 2713	. 2 class {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵}
10	4, 9	wceq 1542	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  7087  abrexex2g  7906  marypha2lem4  9340  cshwsiun  17059  cbviunf  32613  iuneq12daf  32614  iunrdx  32621  iunrnmptss  32623  bnj956  34907  bnj1143  34920  bnj1146  34921  bnj1400  34965  bnj882  35056  bnj18eq1  35057  bnj893  35058  bnj1398  35164  iuneq12i  36365  cbviunvw2  36402  cbviundavw  36432  cbviundavw2  36456  ralssiun  37711  volsupnfl  37974  iuneq1i  45503  nfiund  50137  nfiundg  50138