![]() |
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 5037. Theorem uniiun 5062 provides a definition of ordinary union in terms of indexed union. Theorems fniunfv 7257 and funiunfv 7258 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 4997 | . 2 class ∪ 𝑥 ∈ 𝐴 𝐵 |
5 | vy | . . . . . 6 setvar 𝑦 | |
6 | 5 | cv 1532 | . . . . 5 class 𝑦 |
7 | 6, 3 | wcel 2098 | . . . 4 wff 𝑦 ∈ 𝐵 |
8 | 7, 1, 2 | wrex 3059 | . . 3 wff ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 |
9 | 8, 5 | cab 2702 | . 2 class {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵} |
10 | 4, 9 | wceq 1533 | 1 wff ∪ 𝑥 ∈ 𝐴 𝐵 = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵} |
Colors of variables: wff setvar class |
This definition is referenced by: eliun 5001 iuneq12df 5023 nfiun 5027 nfiung 5029 nfiu1OLD 5032 dfiun2g 5034 dfiunv2 5039 cbviun 5040 cbviung 5042 iunssf 5048 iunss 5049 uniiun 5062 iunid 5064 iunsn 5070 iunopab 5561 iunopabOLD 5562 opeliunxp 5745 reliun 5818 fnasrn 7154 abrexex2g 7969 marypha2lem4 9463 cshwsiun 17072 cbviunf 32425 iuneq12daf 32426 iunrdx 32433 iunrnmptss 32435 bnj956 34535 bnj1143 34549 bnj1146 34550 bnj1400 34594 bnj882 34685 bnj18eq1 34686 bnj893 34687 bnj1398 34793 ralssiun 37014 volsupnfl 37266 opeliun2xp 47579 nfiund 48288 nfiundg 48289 |
Copyright terms: Public domain | W3C validator |