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 4997. Theorem uniiun 5022 provides a definition of ordinary union in terms of indexed union. Theorems fniunfv 7221 and funiunfv 7222 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 1539	. . . . 5 class 𝑦
7	6, 3	wcel 2109	. . . 4 wff 𝑦 ∈ 𝐵
8	7, 1, 2	wrex 3053	. . 3 wff ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵
9	8, 5	cab 2707	. 2 class {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵}
10	4, 9	wceq 1540	1 wff ∪ 𝑥 ∈ 𝐴 𝐵 = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵}

This definition is referenced by:  eliun  4959  iuneq12df  4982  iuneq12d  4985  nfiun  4987  nfiung  4989  nfiu1OLD  4992  dfiun2g  4994  dfiunv2  4999  cbviun  5000  cbviung  5002  cbviunv  5004  iunssf  5008  iunss  5009  uniiun  5022  iunid  5024  iunsn  5030  iunopab  5519  iunopabOLD  5520  opeliunxp  5705  opeliun2xp  5706  reliun  5779  fnasrn  7117  abrexex2g  7943  marypha2lem4  9389  cshwsiun  17070  cbviunf  32484  iuneq12daf  32485  iunrdx  32492  iunrnmptss  32494  bnj956  34766  bnj1143  34780  bnj1146  34781  bnj1400  34825  bnj882  34916  bnj18eq1  34917  bnj893  34918  bnj1398  35024  iuneq12i  36183  cbviunvw2  36220  cbviundavw  36250  cbviundavw2  36274  ralssiun  37395  volsupnfl  37659  iuneq1i  45079  nfiund  49660  nfiundg  49661