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

Theorem iunid 4984
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 4557 . . . . 5 {𝑥} = {𝑦𝑦 = 𝑥}
2 equcom 2026 . . . . . 6 (𝑦 = 𝑥𝑥 = 𝑦)
32abbii 2809 . . . . 5 {𝑦𝑦 = 𝑥} = {𝑦𝑥 = 𝑦}
41, 3eqtri 2766 . . . 4 {𝑥} = {𝑦𝑥 = 𝑦}
54a1i 11 . . 3 (𝑥𝐴 → {𝑥} = {𝑦𝑥 = 𝑦})
65iuneq2i 4940 . 2 𝑥𝐴 {𝑥} = 𝑥𝐴 {𝑦𝑥 = 𝑦}
7 iunab 4975 . . 3 𝑥𝐴 {𝑦𝑥 = 𝑦} = {𝑦 ∣ ∃𝑥𝐴 𝑥 = 𝑦}
8 risset 3192 . . . 4 (𝑦𝐴 ↔ ∃𝑥𝐴 𝑥 = 𝑦)
98abbii 2809 . . 3 {𝑦𝑦𝐴} = {𝑦 ∣ ∃𝑥𝐴 𝑥 = 𝑦}
10 abid2 2880 . . 3 {𝑦𝑦𝐴} = 𝐴
117, 9, 103eqtr2i 2772 . 2 𝑥𝐴 {𝑦𝑥 = 𝑦} = 𝐴
126, 11eqtri 2766 1 𝑥𝐴 {𝑥} = 𝐴
Colors of variables: wff setvar class
Syntax hints:   = wceq 1543  wcel 2111  {cab 2715  wrex 3063  {csn 4556   ciun 4919
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2159  ax-12 2176  ax-ext 2709
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-tru 1546  df-ex 1788  df-nf 1792  df-sb 2072  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2887  df-ral 3067  df-rex 3068  df-v 3423  df-in 3888  df-ss 3898  df-sn 4557  df-iun 4921
This theorem is referenced by:  iunxpconst  5636  fvn0ssdmfun  6914  abnexg  7560  xpexgALT  7773  uniqs  8480  dftrpred4g  9365  rankcf  10416  dprd2da  19457  t1ficld  22251  discmp  22322  xkoinjcn  22611  metnrmlem2  23784  ovoliunlem1  24426  i1fima  24602  i1fd  24605  itg1addlem5  24625  fnpreimac  30755  gsumpart  31061  elrspunidl  31347  sibfof  32046  bnj1415  32757  cvmlift2lem12  33015  poimirlem30  35574  itg2addnclem2  35596  ftc1anclem6  35622  uniqsALTV  36231  salexct3  43587  salgensscntex  43589  ctvonmbl  43933  vonct  43937
  Copyright terms: Public domain W3C validator