![]() |
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 4855. Theorem uniiun 4875 provides a definition of ordinary union in terms of indexed union. Theorems fniunfv 6862 and funiunfv 6863 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 4819 | . 2 class ∪ 𝑥 ∈ 𝐴 𝐵 |
5 | vy | . . . . . 6 setvar 𝑦 | |
6 | 5 | cv 1519 | . . . . 5 class 𝑦 |
7 | 6, 3 | wcel 2079 | . . . 4 wff 𝑦 ∈ 𝐵 |
8 | 7, 1, 2 | wrex 3104 | . . 3 wff ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 |
9 | 8, 5 | cab 2773 | . 2 class {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵} |
10 | 4, 9 | wceq 1520 | 1 wff ∪ 𝑥 ∈ 𝐴 𝐵 = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵} |
Colors of variables: wff setvar class |
This definition is referenced by: eliun 4823 iuneq12df 4844 nfiun 4848 nfiu1 4850 dfiunv2 4857 cbviun 4858 iunss 4862 uniiun 4875 iunopab 5326 opeliunxp 5497 reliun 5567 fnasrn 6761 abrexex2g 7512 marypha2lem4 8738 cshwsiun 16250 cbviunf 29976 iuneq12daf 29977 iunrdx 29984 iunrnmptss 29986 bnj956 31621 bnj1143 31635 bnj1146 31636 bnj1400 31680 bnj882 31770 bnj18eq1 31771 bnj893 31772 bnj1398 31876 ralssiun 34165 volsupnfl 34414 iunsn 38598 ss2iundf 39440 iunssf 40843 opeliun2xp 43813 nfiund 44212 |
Copyright terms: Public domain | W3C validator |