Definition df-iun 4999

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 5037. Theorem uniiun 5062 provides a definition of ordinary union in terms of indexed union. Theorems fniunfv 7257 and funiunfv 7258 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 4997	. 2 class ∪ 𝑥 ∈ 𝐴 𝐵
5		vy	. . . . . 6 setvar 𝑦
6	5	cv 1532	. . . . 5 class 𝑦
7	6, 3	wcel 2098	. . . 4 wff 𝑦 ∈ 𝐵
8	7, 1, 2	wrex 3059	. . 3 wff ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵
9	8, 5	cab 2702	. 2 class {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵}
10	4, 9	wceq 1533	1 wff ∪ 𝑥 ∈ 𝐴 𝐵 = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵}

This definition is referenced by:  eliun  5001  iuneq12df  5023  nfiun  5027  nfiung  5029  nfiu1OLD  5032  dfiun2g  5034  dfiunv2  5039  cbviun  5040  cbviung  5042  iunssf  5048  iunss  5049  uniiun  5062  iunid  5064  iunsn  5070  iunopab  5561  iunopabOLD  5562  opeliunxp  5745  reliun  5818  fnasrn  7154  abrexex2g  7969  marypha2lem4  9463  cshwsiun  17072  cbviunf  32425  iuneq12daf  32426  iunrdx  32433  iunrnmptss  32435  bnj956  34535  bnj1143  34549  bnj1146  34550  bnj1400  34594  bnj882  34685  bnj18eq1  34686  bnj893  34687  bnj1398  34793  ralssiun  37014  volsupnfl  37266  opeliun2xp  47579  nfiund  48288  nfiundg  48289