Definition df-iun 4936

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 4975. Theorem uniiun 5002 provides a definition of ordinary union in terms of indexed union. Theorems fniunfv 7199 and funiunfv 7200 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 4934	. 2 class ∪ 𝑥 ∈ 𝐴 𝐵
5		vy	. . . . . 6 setvar 𝑦
6	5	cv 1541	. . . . 5 class 𝑦
7	6, 3	wcel 2114	. . . 4 wff 𝑦 ∈ 𝐵
8	7, 1, 2	wrex 3062	. . 3 wff ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵
9	8, 5	cab 2715	. 2 class {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵}
10	4, 9	wceq 1542	1 wff ∪ 𝑥 ∈ 𝐴 𝐵 = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵}

This definition is referenced by:  eliun  4938  iuneq12df  4961  iuneq12d  4964  nfiun  4966  nfiung  4968  nfiu1OLD  4971  dfiun2g  4973  dfiunv2  4977  cbviun  4978  cbviung  4980  cbviunv  4982  iunssfOLD  4987  iunssOLD  4989  uniiun  5002  iunid  5004  iunsn  5009  iunopab  5511  opeliunxp  5695  opeliun2xp  5696  fnasrn  7096  abrexex2g  7914  marypha2lem4  9348  cshwsiun  17067  cbviunf  32622  iuneq12daf  32623  iunrdx  32630  iunrnmptss  32632  bnj956  34916  bnj1143  34929  bnj1146  34930  bnj1400  34974  bnj882  35065  bnj18eq1  35066  bnj893  35067  bnj1398  35173  iuneq12i  36374  cbviunvw2  36411  cbviundavw  36441  cbviundavw2  36465  ralssiun  37720  volsupnfl  37983  iuneq1i  45512  nfiund  50140  nfiundg  50141