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

Theorem iunid 4957
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 4541 . . . . 5 {𝑥} = {𝑦𝑦 = 𝑥}
2 equcom 2026 . . . . . 6 (𝑦 = 𝑥𝑥 = 𝑦)
32abbii 2886 . . . . 5 {𝑦𝑦 = 𝑥} = {𝑦𝑥 = 𝑦}
41, 3eqtri 2844 . . . 4 {𝑥} = {𝑦𝑥 = 𝑦}
54a1i 11 . . 3 (𝑥𝐴 → {𝑥} = {𝑦𝑥 = 𝑦})
65iuneq2i 4913 . 2 𝑥𝐴 {𝑥} = 𝑥𝐴 {𝑦𝑥 = 𝑦}
7 iunab 4948 . . 3 𝑥𝐴 {𝑦𝑥 = 𝑦} = {𝑦 ∣ ∃𝑥𝐴 𝑥 = 𝑦}
8 risset 3253 . . . 4 (𝑦𝐴 ↔ ∃𝑥𝐴 𝑥 = 𝑦)
98abbii 2886 . . 3 {𝑦𝑦𝐴} = {𝑦 ∣ ∃𝑥𝐴 𝑥 = 𝑦}
10 abid2 2954 . . 3 {𝑦𝑦𝐴} = 𝐴
117, 9, 103eqtr2i 2850 . 2 𝑥𝐴 {𝑦𝑥 = 𝑦} = 𝐴
126, 11eqtri 2844 1 𝑥𝐴 {𝑥} = 𝐴
Colors of variables: wff setvar class
Syntax hints:   = wceq 1538  wcel 2115  {cab 2799  wrex 3127  {csn 4540   ciun 4892
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2178  ax-ext 2793
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2071  df-clab 2800  df-cleq 2814  df-clel 2892  df-nfc 2960  df-ral 3131  df-rex 3132  df-v 3473  df-in 3917  df-ss 3927  df-sn 4541  df-iun 4894
This theorem is referenced by:  iunxpconst  5597  fvn0ssdmfun  6815  abnexg  7453  xpexgALT  7657  uniqs  8332  rankcf  10176  dprd2da  19143  t1ficld  21911  discmp  21982  xkoinjcn  22271  metnrmlem2  23444  ovoliunlem1  24085  i1fima  24261  i1fd  24264  itg1addlem5  24283  fnpreimac  30403  sibfof  31606  bnj1415  32318  cvmlift2lem12  32569  dftrpred4g  33081  poimirlem30  34969  itg2addnclem2  34991  ftc1anclem6  35017  uniqsALTV  35628  salexct3  42801  salgensscntex  42803  ctvonmbl  43147  vonct  43151
  Copyright terms: Public domain W3C validator