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

Theorem iunid 4795
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 4398 . . . . 5 {𝑥} = {𝑦𝑦 = 𝑥}
2 equcom 2122 . . . . . 6 (𝑦 = 𝑥𝑥 = 𝑦)
32abbii 2944 . . . . 5 {𝑦𝑦 = 𝑥} = {𝑦𝑥 = 𝑦}
41, 3eqtri 2849 . . . 4 {𝑥} = {𝑦𝑥 = 𝑦}
54a1i 11 . . 3 (𝑥𝐴 → {𝑥} = {𝑦𝑥 = 𝑦})
65iuneq2i 4759 . 2 𝑥𝐴 {𝑥} = 𝑥𝐴 {𝑦𝑥 = 𝑦}
7 iunab 4786 . . 3 𝑥𝐴 {𝑦𝑥 = 𝑦} = {𝑦 ∣ ∃𝑥𝐴 𝑥 = 𝑦}
8 risset 3272 . . . 4 (𝑦𝐴 ↔ ∃𝑥𝐴 𝑥 = 𝑦)
98abbii 2944 . . 3 {𝑦𝑦𝐴} = {𝑦 ∣ ∃𝑥𝐴 𝑥 = 𝑦}
10 abid2 2950 . . 3 {𝑦𝑦𝐴} = 𝐴
117, 9, 103eqtr2i 2855 . 2 𝑥𝐴 {𝑦𝑥 = 𝑦} = 𝐴
126, 11eqtri 2849 1 𝑥𝐴 {𝑥} = 𝐴
Colors of variables: wff setvar class
Syntax hints:   = wceq 1656  wcel 2164  {cab 2811  wrex 3118  {csn 4397   ciun 4740
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1894  ax-4 1908  ax-5 2009  ax-6 2075  ax-7 2112  ax-9 2173  ax-10 2192  ax-11 2207  ax-12 2220  ax-13 2389  ax-ext 2803
This theorem depends on definitions:  df-bi 199  df-an 387  df-or 879  df-tru 1660  df-ex 1879  df-nf 1883  df-sb 2068  df-clab 2812  df-cleq 2818  df-clel 2821  df-nfc 2958  df-ral 3122  df-rex 3123  df-v 3416  df-in 3805  df-ss 3812  df-sn 4398  df-iun 4742
This theorem is referenced by:  iunxpconst  5408  fvn0ssdmfun  6599  abnexg  7225  xpexgALT  7421  uniqs  8072  rankcf  9914  dprd2da  18795  t1ficld  21502  discmp  21572  xkoinjcn  21861  metnrmlem2  23033  ovoliunlem1  23668  i1fima  23844  i1fd  23847  itg1addlem5  23866  sibfof  30936  bnj1415  31641  cvmlift2lem12  31831  dftrpred4g  32261  poimirlem30  33976  itg2addnclem2  33998  ftc1anclem6  34026  uniqsALTV  34642  salexct3  41344  salgensscntex  41346  ctvonmbl  41690  vonct  41694
  Copyright terms: Public domain W3C validator