![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > iunid | Structured version Visualization version GIF version |
Description: An indexed union of singletons recovers the index set. (Contributed by NM, 6-Sep-2005.) (Proof shortened by SN, 15-Jan-2025.) |
Ref | Expression |
---|---|
iunid | ⊢ ∪ 𝑥 ∈ 𝐴 {𝑥} = 𝐴 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-iun 4998 | . 2 ⊢ ∪ 𝑥 ∈ 𝐴 {𝑥} = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 ∈ {𝑥}} | |
2 | clel5 3665 | . . . 4 ⊢ (𝑦 ∈ 𝐴 ↔ ∃𝑥 ∈ 𝐴 𝑦 = 𝑥) | |
3 | velsn 4647 | . . . . 5 ⊢ (𝑦 ∈ {𝑥} ↔ 𝑦 = 𝑥) | |
4 | 3 | rexbii 3092 | . . . 4 ⊢ (∃𝑥 ∈ 𝐴 𝑦 ∈ {𝑥} ↔ ∃𝑥 ∈ 𝐴 𝑦 = 𝑥) |
5 | 2, 4 | bitr4i 278 | . . 3 ⊢ (𝑦 ∈ 𝐴 ↔ ∃𝑥 ∈ 𝐴 𝑦 ∈ {𝑥}) |
6 | 5 | eqabi 2875 | . 2 ⊢ 𝐴 = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 ∈ {𝑥}} |
7 | 1, 6 | eqtr4i 2766 | 1 ⊢ ∪ 𝑥 ∈ 𝐴 {𝑥} = 𝐴 |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1537 ∈ wcel 2106 {cab 2712 ∃wrex 3068 {csn 4631 ∪ ciun 4996 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1908 ax-6 1965 ax-7 2005 ax-8 2108 ax-9 2116 ax-ext 2706 |
This theorem depends on definitions: df-bi 207 df-an 396 df-tru 1540 df-ex 1777 df-sb 2063 df-clab 2713 df-cleq 2727 df-clel 2814 df-rex 3069 df-v 3480 df-sn 4632 df-iun 4998 |
This theorem is referenced by: iunxpconst 5761 fvn0ssdmfun 7094 abnexg 7775 xpexgALT 8005 uniqs 8816 rankcf 10815 dprd2da 20077 t1ficld 23351 discmp 23422 xkoinjcn 23711 metnrmlem2 24896 ovoliunlem1 25551 i1fima 25727 i1fd 25730 itg1addlem5 25750 dmdju 32664 fnpreimac 32688 gsumpart 33043 elrspunidl 33436 sibfof 34322 bnj1415 35031 cvmlift2lem12 35299 poimirlem30 37637 itg2addnclem2 37659 ftc1anclem6 37685 uniqsALTV 38311 salexct3 46298 salgensscntex 46300 ctvonmbl 46645 vonct 46649 |
Copyright terms: Public domain | W3C validator |