![]() |
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 5035. Theorem uniiun 5060 provides a definition of ordinary union in terms of indexed union. Theorems fniunfv 7248 and funiunfv 7249 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 4996 | . 2 class ∪ 𝑥 ∈ 𝐴 𝐵 |
5 | vy | . . . . . 6 setvar 𝑦 | |
6 | 5 | cv 1538 | . . . . 5 class 𝑦 |
7 | 6, 3 | wcel 2104 | . . . 4 wff 𝑦 ∈ 𝐵 |
8 | 7, 1, 2 | wrex 3068 | . . 3 wff ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 |
9 | 8, 5 | cab 2707 | . 2 class {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵} |
10 | 4, 9 | wceq 1539 | 1 wff ∪ 𝑥 ∈ 𝐴 𝐵 = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵} |
Colors of variables: wff setvar class |
This definition is referenced by: eliun 5000 iuneq12df 5022 nfiun 5026 nfiung 5028 nfiu1 5030 dfiun2g 5032 dfiunv2 5037 cbviun 5038 cbviung 5040 iunssf 5046 iunss 5047 uniiun 5060 iunid 5062 iunsn 5068 iunopab 5558 iunopabOLD 5559 opeliunxp 5742 reliun 5815 fnasrn 7144 abrexex2g 7953 marypha2lem4 9435 cshwsiun 17037 cbviunf 32054 iuneq12daf 32055 iunrdx 32062 iunrnmptss 32064 bnj956 34085 bnj1143 34099 bnj1146 34100 bnj1400 34144 bnj882 34235 bnj18eq1 34236 bnj893 34237 bnj1398 34343 ralssiun 36591 volsupnfl 36836 opeliun2xp 47096 nfiund 47806 nfiundg 47807 |
Copyright terms: Public domain | W3C validator |