![]() |
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 7246 and funiunfv 7247 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 4998 | . 2 class ∪ 𝑥 ∈ 𝐴 𝐵 |
5 | vy | . . . . . 6 setvar 𝑦 | |
6 | 5 | cv 1541 | . . . . 5 class 𝑦 |
7 | 6, 3 | wcel 2107 | . . . 4 wff 𝑦 ∈ 𝐵 |
8 | 7, 1, 2 | wrex 3071 | . . 3 wff ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵 |
9 | 8, 5 | cab 2710 | . 2 class {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵} |
10 | 4, 9 | wceq 1542 | 1 wff ∪ 𝑥 ∈ 𝐴 𝐵 = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 ∈ 𝐵} |
Colors of variables: wff setvar class |
This definition is referenced by: eliun 5002 iuneq12df 5024 nfiun 5028 nfiung 5030 nfiu1 5032 dfiun2g 5034 dfiunv2 5039 cbviun 5040 cbviung 5042 iunssf 5048 iunss 5049 uniiun 5062 iunid 5064 iunsn 5070 iunopab 5560 iunopabOLD 5561 opeliunxp 5744 reliun 5817 fnasrn 7143 abrexex2g 7951 marypha2lem4 9433 cshwsiun 17033 cbviunf 31787 iuneq12daf 31788 iunrdx 31795 iunrnmptss 31797 bnj956 33787 bnj1143 33801 bnj1146 33802 bnj1400 33846 bnj882 33937 bnj18eq1 33938 bnj893 33939 bnj1398 34045 ralssiun 36288 volsupnfl 36533 opeliun2xp 47008 nfiund 47719 nfiundg 47720 |
Copyright terms: Public domain | W3C validator |