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

Theorem iunid 4324
Description: An indexed union of singletons recovers the index set. (Contributed by NM, 6-Sep-2005.)
Assertion
Ref Expression
iunid  |-  U_ x  e.  A  { x }  =  A
Distinct variable group:    x, A

Proof of Theorem iunid
Dummy variable  y is distinct from all other variables.
StepHypRef Expression
1 df-sn 3960 . . . . 5  |-  { x }  =  { y  |  y  =  x }
2 equcom 1870 . . . . . 6  |-  ( y  =  x  <->  x  =  y )
32abbii 2587 . . . . 5  |-  { y  |  y  =  x }  =  { y  |  x  =  y }
41, 3eqtri 2493 . . . 4  |-  { x }  =  { y  |  x  =  y }
54a1i 11 . . 3  |-  ( x  e.  A  ->  { x }  =  { y  |  x  =  y } )
65iuneq2i 4288 . 2  |-  U_ x  e.  A  { x }  =  U_ x  e.  A  { y  |  x  =  y }
7 iunab 4315 . . 3  |-  U_ x  e.  A  { y  |  x  =  y }  =  { y  |  E. x  e.  A  x  =  y }
8 risset 2902 . . . 4  |-  ( y  e.  A  <->  E. x  e.  A  x  =  y )
98abbii 2587 . . 3  |-  { y  |  y  e.  A }  =  { y  |  E. x  e.  A  x  =  y }
10 abid2 2593 . . 3  |-  { y  |  y  e.  A }  =  A
117, 9, 103eqtr2i 2499 . 2  |-  U_ x  e.  A  { y  |  x  =  y }  =  A
126, 11eqtri 2493 1  |-  U_ x  e.  A  { x }  =  A
Colors of variables: wff setvar class
Syntax hints:    = wceq 1452    e. wcel 1904   {cab 2457   E.wrex 2757   {csn 3959   U_ciun 4269
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451
This theorem depends on definitions:  df-bi 190  df-or 377  df-an 378  df-tru 1455  df-ex 1672  df-nf 1676  df-sb 1806  df-clab 2458  df-cleq 2464  df-clel 2467  df-nfc 2601  df-ral 2761  df-rex 2762  df-v 3033  df-in 3397  df-ss 3404  df-sn 3960  df-iun 4271
This theorem is referenced by:  iunxpconst  4896  fvn0ssdmfun  6028  xpexgALT  6805  uniqs  7441  rankcf  9220  dprd2da  17753  t1ficld  20420  discmp  20490  xkoinjcn  20779  metnrmlem2  21955  metnrmlem2OLD  21970  ovoliunlem1  22533  i1fima  22715  i1fd  22718  itg1addlem5  22737  sibfof  29246  bnj1415  29919  cvmlift2lem12  30109  dftrpred4g  30546  poimirlem30  32034  itg2addnclem2  32058  ftc1anclem6  32086  salexct3  38313  salgensscntex  38315
  Copyright terms: Public domain W3C validator