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

Theorem iunid 4767
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 4371 . . . . 5 {𝑥} = {𝑦𝑦 = 𝑥}
2 equcom 2114 . . . . . 6 (𝑦 = 𝑥𝑥 = 𝑦)
32abbii 2923 . . . . 5 {𝑦𝑦 = 𝑥} = {𝑦𝑥 = 𝑦}
41, 3eqtri 2828 . . . 4 {𝑥} = {𝑦𝑥 = 𝑦}
54a1i 11 . . 3 (𝑥𝐴 → {𝑥} = {𝑦𝑥 = 𝑦})
65iuneq2i 4731 . 2 𝑥𝐴 {𝑥} = 𝑥𝐴 {𝑦𝑥 = 𝑦}
7 iunab 4758 . . 3 𝑥𝐴 {𝑦𝑥 = 𝑦} = {𝑦 ∣ ∃𝑥𝐴 𝑥 = 𝑦}
8 risset 3250 . . . 4 (𝑦𝐴 ↔ ∃𝑥𝐴 𝑥 = 𝑦)
98abbii 2923 . . 3 {𝑦𝑦𝐴} = {𝑦 ∣ ∃𝑥𝐴 𝑥 = 𝑦}
10 abid2 2929 . . 3 {𝑦𝑦𝐴} = 𝐴
117, 9, 103eqtr2i 2834 . 2 𝑥𝐴 {𝑦𝑥 = 𝑦} = 𝐴
126, 11eqtri 2828 1 𝑥𝐴 {𝑥} = 𝐴
Colors of variables: wff setvar class
Syntax hints:   = wceq 1637  wcel 2156  {cab 2792  wrex 3097  {csn 4370   ciun 4712
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-13 2420  ax-ext 2784
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2061  df-clab 2793  df-cleq 2799  df-clel 2802  df-nfc 2937  df-ral 3101  df-rex 3102  df-v 3393  df-in 3776  df-ss 3783  df-sn 4371  df-iun 4714
This theorem is referenced by:  iunxpconst  5375  fvn0ssdmfun  6572  abnexg  7194  xpexgALT  7391  uniqs  8042  rankcf  9884  dprd2da  18643  t1ficld  21345  discmp  21415  xkoinjcn  21704  metnrmlem2  22876  ovoliunlem1  23483  i1fima  23659  i1fd  23662  itg1addlem5  23681  sibfof  30727  bnj1415  31429  cvmlift2lem12  31619  dftrpred4g  32054  poimirlem30  33752  itg2addnclem2  33774  ftc1anclem6  33802  uniqsALTV  34416  salexct3  41039  salgensscntex  41041  ctvonmbl  41385  vonct  41389
  Copyright terms: Public domain W3C validator