Definition df-iun 4949

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

This definition is referenced by:  eliun  4951  iuneq12df  4974  iuneq12d  4977  nfiun  4979  nfiung  4981  nfiu1OLD  4984  dfiun2g  4986  dfiunv2  4990  cbviun  4991  cbviung  4993  cbviunv  4995  iunssfOLD  5000  iunssOLD  5002  uniiun  5015  iunid  5017  iunsn  5022  iunopab  5508  opeliunxp  5692  opeliun2xp  5693  fnasrn  7092  abrexex2g  7910  marypha2lem4  9345  cshwsiun  17031  cbviunf  32633  iuneq12daf  32634  iunrdx  32641  iunrnmptss  32643  bnj956  34934  bnj1143  34948  bnj1146  34949  bnj1400  34993  bnj882  35084  bnj18eq1  35085  bnj893  35086  bnj1398  35192  iuneq12i  36391  cbviunvw2  36428  cbviundavw  36458  cbviundavw2  36482  ralssiun  37614  volsupnfl  37868  iuneq1i  45396  nfiund  49986  nfiundg  49987