Definition df-iun 5017

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 5056. Theorem uniiun 5081 provides a definition of ordinary union in terms of indexed union. Theorems fniunfv 7284 and funiunfv 7285 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 5015	. 2 class ∪ 𝑥 ∈ 𝐴 𝐵
5		vy	. . . . . 6 setvar 𝑦
6	5	cv 1536	. . . . 5 class 𝑦
7	6, 3	wcel 2108	. . . 4 wff 𝑦 ∈ 𝐵
8	7, 1, 2	wrex 3076	. . 3 wff ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵
9	8, 5	cab 2717	. 2 class {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵}
10	4, 9	wceq 1537	1 wff ∪ 𝑥 ∈ 𝐴 𝐵 = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵}

This definition is referenced by:  eliun  5019  iuneq12df  5041  iuneq12d  5044  nfiun  5046  nfiung  5048  nfiu1OLD  5051  dfiun2g  5053  dfiunv2  5058  cbviun  5059  cbviung  5061  cbviunv  5063  iunssf  5067  iunss  5068  uniiun  5081  iunid  5083  iunsn  5089  iunopab  5578  iunopabOLD  5579  opeliunxp  5767  reliun  5840  fnasrn  7179  abrexex2g  8005  marypha2lem4  9507  cshwsiun  17147  cbviunf  32578  iuneq12daf  32579  iunrdx  32586  iunrnmptss  32588  bnj956  34752  bnj1143  34766  bnj1146  34767  bnj1400  34811  bnj882  34902  bnj18eq1  34903  bnj893  34904  bnj1398  35010  iuneq12i  36159  cbviunvw2  36198  cbviundavw  36228  cbviundavw2  36252  ralssiun  37373  volsupnfl  37625  iuneq1i  44987  opeliun2xp  48057  nfiund  48766  nfiundg  48767