![]() |
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 4990 | . 2 ⊢ ∪ 𝑥 ∈ 𝐴 {𝑥} = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 ∈ {𝑥}} | |
2 | clel5 3648 | . . . 4 ⊢ (𝑦 ∈ 𝐴 ↔ ∃𝑥 ∈ 𝐴 𝑦 = 𝑥) | |
3 | velsn 4637 | . . . . 5 ⊢ (𝑦 ∈ {𝑥} ↔ 𝑦 = 𝑥) | |
4 | 3 | rexbii 3086 | . . . 4 ⊢ (∃𝑥 ∈ 𝐴 𝑦 ∈ {𝑥} ↔ ∃𝑥 ∈ 𝐴 𝑦 = 𝑥) |
5 | 2, 4 | bitr4i 278 | . . 3 ⊢ (𝑦 ∈ 𝐴 ↔ ∃𝑥 ∈ 𝐴 𝑦 ∈ {𝑥}) |
6 | 5 | eqabi 2861 | . 2 ⊢ 𝐴 = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 ∈ {𝑥}} |
7 | 1, 6 | eqtr4i 2755 | 1 ⊢ ∪ 𝑥 ∈ 𝐴 {𝑥} = 𝐴 |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1533 ∈ wcel 2098 {cab 2701 ∃wrex 3062 {csn 4621 ∪ ciun 4988 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-ext 2695 |
This theorem depends on definitions: df-bi 206 df-an 396 df-tru 1536 df-ex 1774 df-sb 2060 df-clab 2702 df-cleq 2716 df-clel 2802 df-rex 3063 df-v 3468 df-sn 4622 df-iun 4990 |
This theorem is referenced by: iunxpconst 5739 fvn0ssdmfun 7067 abnexg 7737 xpexgALT 7962 uniqs 8768 rankcf 10769 dprd2da 19956 t1ficld 23155 discmp 23226 xkoinjcn 23515 metnrmlem2 24700 ovoliunlem1 25355 i1fima 25531 i1fd 25534 itg1addlem5 25554 fnpreimac 32368 gsumpart 32678 elrspunidl 33018 sibfof 33831 bnj1415 34540 cvmlift2lem12 34796 poimirlem30 37012 itg2addnclem2 37034 ftc1anclem6 37060 uniqsALTV 37692 salexct3 45568 salgensscntex 45570 ctvonmbl 45915 vonct 45919 |
Copyright terms: Public domain | W3C validator |