Definition df-iun 4969

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

This definition is referenced by:  eliun  4971  iuneq12df  4994  iuneq12d  4997  nfiun  4999  nfiung  5001  nfiu1OLD  5004  dfiun2g  5006  dfiunv2  5011  cbviun  5012  cbviung  5014  cbviunv  5016  iunssf  5020  iunss  5021  uniiun  5034  iunid  5036  iunsn  5042  iunopab  5534  iunopabOLD  5535  opeliunxp  5721  opeliun2xp  5722  reliun  5795  fnasrn  7134  abrexex2g  7961  marypha2lem4  9448  cshwsiun  17117  cbviunf  32482  iuneq12daf  32483  iunrdx  32490  iunrnmptss  32492  bnj956  34753  bnj1143  34767  bnj1146  34768  bnj1400  34812  bnj882  34903  bnj18eq1  34904  bnj893  34905  bnj1398  35011  iuneq12i  36159  cbviunvw2  36196  cbviundavw  36226  cbviundavw2  36250  ralssiun  37371  volsupnfl  37635  iuneq1i  45057  nfiund  49486  nfiundg  49487