Definition df-iun 4993

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 5033. Theorem uniiun 5058 provides a definition of ordinary union in terms of indexed union. Theorems fniunfv 7267 and funiunfv 7268 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 4991	. 2 class ∪ 𝑥 ∈ 𝐴 𝐵
5		vy	. . . . . 6 setvar 𝑦
6	5	cv 1539	. . . . 5 class 𝑦
7	6, 3	wcel 2108	. . . 4 wff 𝑦 ∈ 𝐵
8	7, 1, 2	wrex 3070	. . 3 wff ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵
9	8, 5	cab 2714	. 2 class {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵}
10	4, 9	wceq 1540	1 wff ∪ 𝑥 ∈ 𝐴 𝐵 = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵}

This definition is referenced by:  eliun  4995  iuneq12df  5018  iuneq12d  5021  nfiun  5023  nfiung  5025  nfiu1OLD  5028  dfiun2g  5030  dfiunv2  5035  cbviun  5036  cbviung  5038  cbviunv  5040  iunssf  5044  iunss  5045  uniiun  5058  iunid  5060  iunsn  5066  iunopab  5564  iunopabOLD  5565  opeliunxp  5752  opeliun2xp  5753  reliun  5826  fnasrn  7165  abrexex2g  7989  marypha2lem4  9478  cshwsiun  17137  cbviunf  32568  iuneq12daf  32569  iunrdx  32576  iunrnmptss  32578  bnj956  34790  bnj1143  34804  bnj1146  34805  bnj1400  34849  bnj882  34940  bnj18eq1  34941  bnj893  34942  bnj1398  35048  iuneq12i  36196  cbviunvw2  36233  cbviundavw  36263  cbviundavw2  36287  ralssiun  37408  volsupnfl  37672  iuneq1i  45090  nfiund  49193  nfiundg  49194