| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > df-iun | Structured version Visualization version GIF version | ||
| 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 5033. Theorem uniiun 5058 provides a definition of ordinary union in terms of indexed union. Theorems fniunfv 7267 and funiunfv 7268 are useful when 𝐵 is a function. (Contributed by NM, 27-Jun-1998.) |
| Ref | Expression |
|---|---|
| df-iun | ⊢ ∪ 𝑥 ∈ 𝐴 𝐵 = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵} |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | vx | . . 3 setvar 𝑥 | |
| 2 | cA | . . 3 class 𝐴 | |
| 3 | cB | . . 3 class 𝐵 | |
| 4 | 1, 2, 3 | ciun 4991 | . 2 class ∪ 𝑥 ∈ 𝐴 𝐵 |
| 5 | vy | . . . . . 6 setvar 𝑦 | |
| 6 | 5 | cv 1539 | . . . . 5 class 𝑦 |
| 7 | 6, 3 | wcel 2108 | . . . 4 wff 𝑦 ∈ 𝐵 |
| 8 | 7, 1, 2 | wrex 3070 | . . 3 wff ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 |
| 9 | 8, 5 | cab 2714 | . 2 class {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵} |
| 10 | 4, 9 | wceq 1540 | 1 wff ∪ 𝑥 ∈ 𝐴 𝐵 = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵} |
| Colors of variables: wff setvar class |
| This definition is referenced by: eliun 4995 iuneq12df 5018 iuneq12d 5021 nfiun 5023 nfiung 5025 nfiu1OLD 5028 dfiun2g 5030 dfiunv2 5035 cbviun 5036 cbviung 5038 cbviunv 5040 iunssf 5044 iunss 5045 uniiun 5058 iunid 5060 iunsn 5066 iunopab 5564 iunopabOLD 5565 opeliunxp 5752 opeliun2xp 5753 reliun 5826 fnasrn 7165 abrexex2g 7989 marypha2lem4 9478 cshwsiun 17137 cbviunf 32568 iuneq12daf 32569 iunrdx 32576 iunrnmptss 32578 bnj956 34790 bnj1143 34804 bnj1146 34805 bnj1400 34849 bnj882 34940 bnj18eq1 34941 bnj893 34942 bnj1398 35048 iuneq12i 36196 cbviunvw2 36233 cbviundavw 36263 cbviundavw2 36287 ralssiun 37408 volsupnfl 37672 iuneq1i 45090 nfiund 49193 nfiundg 49194 |
| Copyright terms: Public domain | W3C validator |