Theorem iunid 4575

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.

Step	Hyp	Ref	Expression
1		df-sn 4178	. . . . 5 |- { x } = { y | y = x }
2		equcom 1945	. . . . . 6 |- ( y = x <-> x = y )
3	2	abbii 2739	. . . . 5 |- { y | y = x } = { y | x = y }
4	1, 3	eqtri 2644	. . . 4 |- { x } = { y | x = y }
5	4	a1i 11	. . 3 |- ( x e. A -> { x } = { y | x = y } )
6	5	iuneq2i 4539	. 2 |- U_ x e. A { x } = U_ x e. A { y | x = y }
7		iunab 4566	. . 3 |- U_ x e. A { y | x = y } = { y | E. x e. A x = y }
8		risset 3062	. . . 4 |- ( y e. A <-> E. x e. A x = y )
9	8	abbii 2739	. . 3 |- { y | y e. A } = { y | E. x e. A x = y }
10		abid2 2745	. . 3 |- { y | y e. A } = A
11	7, 9, 10	3eqtr2i 2650	. 2 |- U_ x e. A { y | x = y } = A
12	6, 11	eqtri 2644	1 |- U_ x e. A { x } = A

Syntax hints:   = wceq 1483   e. wcel 1990   {cab 2608   E.wrex 2913   {csn 4177   U_ciun 4520

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ral 2917  df-rex 2918  df-v 3202  df-in 3581  df-ss 3588  df-sn 4178  df-iun 4522

This theorem is referenced by:  iunxpconst  5175  fvn0ssdmfun  6350  abnexg  6964  xpexgALT  7161  uniqs  7807  rankcf  9599  dprd2da  18441  t1ficld  21131  discmp  21201  xkoinjcn  21490  metnrmlem2  22663  ovoliunlem1  23270  i1fima  23445  i1fd  23448  itg1addlem5  23467  sibfof  30402  bnj1415  31106  cvmlift2lem12  31296  dftrpred4g  31734  poimirlem30  33439  itg2addnclem2  33462  ftc1anclem6  33490  uniqsALTV  34101  salexct3  40560  salgensscntex  40562  ctvonmbl  40903  vonct  40907