Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  iunid Structured version   Visualization version   GIF version

Theorem iunid 4511
 Description: An indexed union of singletons recovers the index set. (Contributed by NM, 6-Sep-2005.)
Assertion
Ref Expression
iunid 𝑥𝐴 {𝑥} = 𝐴
Distinct variable group:   𝑥,𝐴

Proof of Theorem iunid
Dummy variable 𝑦 is distinct from all other variables.
StepHypRef Expression
1 df-sn 4126 . . . . 5 {𝑥} = {𝑦𝑦 = 𝑥}
2 equcom 1932 . . . . . 6 (𝑦 = 𝑥𝑥 = 𝑦)
32abbii 2726 . . . . 5 {𝑦𝑦 = 𝑥} = {𝑦𝑥 = 𝑦}
41, 3eqtri 2632 . . . 4 {𝑥} = {𝑦𝑥 = 𝑦}
54a1i 11 . . 3 (𝑥𝐴 → {𝑥} = {𝑦𝑥 = 𝑦})
65iuneq2i 4475 . 2 𝑥𝐴 {𝑥} = 𝑥𝐴 {𝑦𝑥 = 𝑦}
7 iunab 4502 . . 3 𝑥𝐴 {𝑦𝑥 = 𝑦} = {𝑦 ∣ ∃𝑥𝐴 𝑥 = 𝑦}
8 risset 3044 . . . 4 (𝑦𝐴 ↔ ∃𝑥𝐴 𝑥 = 𝑦)
98abbii 2726 . . 3 {𝑦𝑦𝐴} = {𝑦 ∣ ∃𝑥𝐴 𝑥 = 𝑦}
10 abid2 2732 . . 3 {𝑦𝑦𝐴} = 𝐴
117, 9, 103eqtr2i 2638 . 2 𝑥𝐴 {𝑦𝑥 = 𝑦} = 𝐴
126, 11eqtri 2632 1 𝑥𝐴 {𝑥} = 𝐴
 Colors of variables: wff setvar class Syntax hints:   = wceq 1475   ∈ wcel 1977  {cab 2596  ∃wrex 2897  {csn 4125  ∪ ciun 4455 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ral 2901  df-rex 2902  df-v 3175  df-in 3547  df-ss 3554  df-sn 4126  df-iun 4457 This theorem is referenced by:  iunxpconst  5098  fvn0ssdmfun  6258  xpexgALT  7052  uniqs  7694  rankcf  9478  dprd2da  18264  t1ficld  20941  discmp  21011  xkoinjcn  21300  metnrmlem2  22471  ovoliunlem1  23077  i1fima  23251  i1fd  23254  itg1addlem5  23273  sibfof  29729  bnj1415  30360  cvmlift2lem12  30550  dftrpred4g  30978  poimirlem30  32609  itg2addnclem2  32632  ftc1anclem6  32660  salexct3  39236  salgensscntex  39238  ctvonmbl  39580  vonct  39584
 Copyright terms: Public domain W3C validator