Definition df-iun 4956

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 4994. Theorem uniiun 5021 provides a definition of ordinary union in terms of indexed union. Theorems fniunfv 7248 and funiunfv 7249 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 4954	. 2 class ∪ 𝑥 ∈ 𝐴 𝐵
5		vy	. . . . . 6 setvar 𝑦
6	5	cv 1569	. . . . 5 class 𝑦
7	6, 3	wcel 2145	. . . 4 wff 𝑦 ∈ 𝐵
8	7, 1, 2	wrex 3088	. . 3 wff ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵
9	8, 5	cab 2740	. 2 class {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵}
10	4, 9	wceq 1570	1 wff ∪ 𝑥 ∈ 𝐴 𝐵 = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵}

This definition is used by:  eliun  4958  iuneq12df  4981  iuneq12d  4984  nfiun  4986  nfiung  4988  dfiun2g  4992  dfiunv2  4996  cbviun  4997  cbviung  4999  cbviunv  5001  iunssfOLD  5006  iunssOLD  5008  uniiun  5021  iunid  5023  iunsn  5028  iunopab  5542  opeliunxp  5726  opeliun2xp  5727  fnasrn  7145  abrexex2g  7965  marypha2lem4  9412  cshwsiun  17197  cbviunf  33037  iuneq12daf  33038  iunrdx  33045  iunrnmptss  33046  bnj956  35294  bnj1143  35307  bnj1146  35308  bnj1400  35352  bnj882  35443  bnj18eq1  35444  bnj893  35445  bnj1398  35551  iuneq12i  36823  cbviunvw2  36860  cbviundavw  36890  cbviundavw2  36914  ralssiun  38169  volsupnfl  38422  iuneq1i  45926  nfiund  50608  nfiundg  50609