Definition df-iun 4943

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 4982. Theorem uniiun 5007 provides a definition of ordinary union in terms of indexed union. Theorems fniunfv 7183 and funiunfv 7184 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 4941	. 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  4945  iuneq12df  4968  iuneq12d  4971  nfiun  4973  nfiung  4975  nfiu1OLD  4978  dfiun2g  4980  dfiunv2  4984  cbviun  4985  cbviung  4987  cbviunv  4989  iunssf  4993  iunss  4994  uniiun  5007  iunid  5009  iunsn  5015  iunopab  5502  opeliunxp  5686  opeliun2xp  5687  reliun  5759  fnasrn  7079  abrexex2g  7899  marypha2lem4  9328  cshwsiun  17011  cbviunf  32499  iuneq12daf  32500  iunrdx  32507  iunrnmptss  32509  bnj956  34749  bnj1143  34763  bnj1146  34764  bnj1400  34808  bnj882  34899  bnj18eq1  34900  bnj893  34901  bnj1398  35007  iuneq12i  36179  cbviunvw2  36216  cbviundavw  36246  cbviundavw2  36270  ralssiun  37391  volsupnfl  37655  iuneq1i  45073  nfiund  49669  nfiundg  49670