![]() |
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 5000 | . 2 ⊢ ∪ 𝑥 ∈ 𝐴 {𝑥} = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 ∈ {𝑥}} | |
2 | clel5 3656 | . . . 4 ⊢ (𝑦 ∈ 𝐴 ↔ ∃𝑥 ∈ 𝐴 𝑦 = 𝑥) | |
3 | velsn 4645 | . . . . 5 ⊢ (𝑦 ∈ {𝑥} ↔ 𝑦 = 𝑥) | |
4 | 3 | rexbii 3095 | . . . 4 ⊢ (∃𝑥 ∈ 𝐴 𝑦 ∈ {𝑥} ↔ ∃𝑥 ∈ 𝐴 𝑦 = 𝑥) |
5 | 2, 4 | bitr4i 278 | . . 3 ⊢ (𝑦 ∈ 𝐴 ↔ ∃𝑥 ∈ 𝐴 𝑦 ∈ {𝑥}) |
6 | 5 | eqabi 2870 | . 2 ⊢ 𝐴 = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 ∈ {𝑥}} |
7 | 1, 6 | eqtr4i 2764 | 1 ⊢ ∪ 𝑥 ∈ 𝐴 {𝑥} = 𝐴 |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1542 ∈ wcel 2107 {cab 2710 ∃wrex 3071 {csn 4629 ∪ ciun 4998 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-ext 2704 |
This theorem depends on definitions: df-bi 206 df-an 398 df-tru 1545 df-ex 1783 df-sb 2069 df-clab 2711 df-cleq 2725 df-clel 2811 df-rex 3072 df-v 3477 df-sn 4630 df-iun 5000 |
This theorem is referenced by: iunxpconst 5749 fvn0ssdmfun 7077 abnexg 7743 xpexgALT 7968 uniqs 8771 rankcf 10772 dprd2da 19912 t1ficld 22831 discmp 22902 xkoinjcn 23191 metnrmlem2 24376 ovoliunlem1 25019 i1fima 25195 i1fd 25198 itg1addlem5 25218 fnpreimac 31896 gsumpart 32207 elrspunidl 32546 sibfof 33339 bnj1415 34049 cvmlift2lem12 34305 poimirlem30 36518 itg2addnclem2 36540 ftc1anclem6 36566 uniqsALTV 37198 salexct3 45058 salgensscntex 45060 ctvonmbl 45405 vonct 45409 |
Copyright terms: Public domain | W3C validator |