Definition df-iun 4999

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 5036. Theorem uniiun 5061 provides a definition of ordinary union in terms of indexed union. Theorems fniunfv 7243 and funiunfv 7244 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 4997	. 2 class ∪ 𝑥 ∈ 𝐴 𝐵
5		vy	. . . . . 6 setvar 𝑦
6	5	cv 1541	. . . . 5 class 𝑦
7	6, 3	wcel 2107	. . . 4 wff 𝑦 ∈ 𝐵
8	7, 1, 2	wrex 3071	. . 3 wff ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵
9	8, 5	cab 2710	. 2 class {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵}
10	4, 9	wceq 1542	1 wff ∪ 𝑥 ∈ 𝐴 𝐵 = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵}

This definition is referenced by:  eliun  5001  iuneq12df  5023  nfiun  5027  nfiung  5029  nfiu1  5031  dfiun2g  5033  dfiunv2  5038  cbviun  5039  cbviung  5041  iunssf  5047  iunss  5048  uniiun  5061  iunid  5063  iunsn  5069  iunopab  5559  iunopabOLD  5560  opeliunxp  5742  reliun  5815  fnasrn  7140  abrexex2g  7948  marypha2lem4  9430  cshwsiun  17030  cbviunf  31775  iuneq12daf  31776  iunrdx  31783  iunrnmptss  31785  bnj956  33776  bnj1143  33790  bnj1146  33791  bnj1400  33835  bnj882  33926  bnj18eq1  33927  bnj893  33928  bnj1398  34034  ralssiun  36277  volsupnfl  36522  opeliun2xp  46962  nfiund  47673  nfiundg  47674