Definition df-iun 4941

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 4980. Theorem uniiun 5005 provides a definition of ordinary union in terms of indexed union. Theorems fniunfv 7181 and funiunfv 7182 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 4939	. 2 class ∪ 𝑥 ∈ 𝐴 𝐵
5		vy	. . . . . 6 setvar 𝑦
6	5	cv 1540	. . . . 5 class 𝑦
7	6, 3	wcel 2111	. . . 4 wff 𝑦 ∈ 𝐵
8	7, 1, 2	wrex 3056	. . 3 wff ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵
9	8, 5	cab 2709	. 2 class {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵}
10	4, 9	wceq 1541	1 wff ∪ 𝑥 ∈ 𝐴 𝐵 = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵}

This definition is referenced by:  eliun  4943  iuneq12df  4966  iuneq12d  4969  nfiun  4971  nfiung  4973  nfiu1OLD  4976  dfiun2g  4978  dfiunv2  4982  cbviun  4983  cbviung  4985  cbviunv  4987  iunssf  4991  iunss  4992  uniiun  5005  iunid  5007  iunsn  5012  iunopab  5497  opeliunxp  5681  opeliun2xp  5682  reliun  5755  fnasrn  7078  abrexex2g  7896  marypha2lem4  9322  cshwsiun  17011  cbviunf  32535  iuneq12daf  32536  iunrdx  32543  iunrnmptss  32545  bnj956  34788  bnj1143  34802  bnj1146  34803  bnj1400  34847  bnj882  34938  bnj18eq1  34939  bnj893  34940  bnj1398  35046  iuneq12i  36239  cbviunvw2  36276  cbviundavw  36306  cbviundavw2  36330  ralssiun  37451  volsupnfl  37715  iuneq1i  45192  nfiund  49785  nfiundg  49786