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

Theorem iunid 4502
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 4122 . . . . 5 {𝑥} = {𝑦𝑦 = 𝑥}
2 equcom 1931 . . . . . 6 (𝑦 = 𝑥𝑥 = 𝑦)
32abbii 2722 . . . . 5 {𝑦𝑦 = 𝑥} = {𝑦𝑥 = 𝑦}
41, 3eqtri 2628 . . . 4 {𝑥} = {𝑦𝑥 = 𝑦}
54a1i 11 . . 3 (𝑥𝐴 → {𝑥} = {𝑦𝑥 = 𝑦})
65iuneq2i 4466 . 2 𝑥𝐴 {𝑥} = 𝑥𝐴 {𝑦𝑥 = 𝑦}
7 iunab 4493 . . 3 𝑥𝐴 {𝑦𝑥 = 𝑦} = {𝑦 ∣ ∃𝑥𝐴 𝑥 = 𝑦}
8 risset 3040 . . . 4 (𝑦𝐴 ↔ ∃𝑥𝐴 𝑥 = 𝑦)
98abbii 2722 . . 3 {𝑦𝑦𝐴} = {𝑦 ∣ ∃𝑥𝐴 𝑥 = 𝑦}
10 abid2 2728 . . 3 {𝑦𝑦𝐴} = 𝐴
117, 9, 103eqtr2i 2634 . 2 𝑥𝐴 {𝑦𝑥 = 𝑦} = 𝐴
126, 11eqtri 2628 1 𝑥𝐴 {𝑥} = 𝐴
Colors of variables: wff setvar class
Syntax hints:   = wceq 1474  wcel 1976  {cab 2592  wrex 2893  {csn 4121   ciun 4446
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2032  ax-13 2229  ax-ext 2586
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2593  df-cleq 2599  df-clel 2602  df-nfc 2736  df-ral 2897  df-rex 2898  df-v 3171  df-in 3543  df-ss 3550  df-sn 4122  df-iun 4448
This theorem is referenced by:  iunxpconst  5085  fvn0ssdmfun  6240  xpexgALT  7026  uniqs  7668  rankcf  9452  dprd2da  18207  t1ficld  20880  discmp  20950  xkoinjcn  21239  metnrmlem2  22399  ovoliunlem1  22991  i1fima  23165  i1fd  23168  itg1addlem5  23187  sibfof  29532  bnj1415  30163  cvmlift2lem12  30353  dftrpred4g  30781  poimirlem30  32409  itg2addnclem2  32432  ftc1anclem6  32460  salexct3  39037  salgensscntex  39039  ctvonmbl  39381  vonct  39385
  Copyright terms: Public domain W3C validator