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 4950. Theorem uniiun 4974 provides a definition of ordinary union in terms of indexed union. Theorems fniunfv 6997 and funiunfv 6998 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 4912 | . 2 class ∪ 𝑥 ∈ 𝐴 𝐵 |
5 | vy | . . . . . 6 setvar 𝑦 | |
6 | 5 | cv 1527 | . . . . 5 class 𝑦 |
7 | 6, 3 | wcel 2105 | . . . 4 wff 𝑦 ∈ 𝐵 |
8 | 7, 1, 2 | wrex 3139 | . . 3 wff ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 |
9 | 8, 5 | cab 2799 | . 2 class {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵} |
10 | 4, 9 | wceq 1528 | 1 wff ∪ 𝑥 ∈ 𝐴 𝐵 = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵} |
Colors of variables: wff setvar class |
This definition is referenced by: eliun 4916 iuneq12df 4937 nfiun 4941 nfiung 4943 nfiu1 4945 dfiunv2 4952 cbviun 4953 cbviung 4955 iunss 4961 uniiun 4974 iunopab 5438 opeliunxp 5613 reliun 5683 fnasrn 6900 abrexex2g 7656 marypha2lem4 8891 cshwsiun 16423 cbviunf 30236 iuneq12daf 30237 iunrdx 30244 iunrnmptss 30246 bnj956 31948 bnj1143 31962 bnj1146 31963 bnj1400 32007 bnj882 32098 bnj18eq1 32099 bnj893 32100 bnj1398 32204 ralssiun 34571 volsupnfl 34819 iunsn 38998 ss2iundf 39884 iunssf 41232 opeliun2xp 44279 nfiund 44675 nfiundg 44676 |
Copyright terms: Public domain | W3C validator |