Theorem iunid 4297

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 3942	. . . . 5 |- { x } = { y | y = x }
2		equcom 1848	. . . . . 6 |- ( y = x <-> x = y )
3	2	abbii 2544	. . . . 5 |- { y | y = x } = { y | x = y }
4	1, 3	eqtri 2450	. . . 4 |- { x } = { y | x = y }
5	4	a1i 11	. . 3 |- ( x e. A -> { x } = { y | x = y } )
6	5	iuneq2i 4261	. 2 |- U_ x e. A { x } = U_ x e. A { y | x = y }
7		iunab 4288	. . 3 |- U_ x e. A { y | x = y } = { y | E. x e. A x = y }
8		risset 2892	. . . 4 |- ( y e. A <-> E. x e. A x = y )
9	8	abbii 2544	. . 3 |- { y | y e. A } = { y | E. x e. A x = y }
10		abid2 2550	. . 3 |- { y | y e. A } = A
11	7, 9, 10	3eqtr2i 2456	. 2 |- U_ x e. A { y | x = y } = A
12	6, 11	eqtri 2450	1 |- U_ x e. A { x } = A

Syntax hints:   = wceq 1437   e. wcel 1872   {cab 2414   E.wrex 2715   {csn 3941   U_ciun 4242

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2063  ax-ext 2408

This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2558  df-ral 2719  df-rex 2720  df-v 3024  df-in 3386  df-ss 3393  df-sn 3942  df-iun 4244

This theorem is referenced by:  iunxpconst  4853  fvn0ssdmfun  5972  xpexgALT  6744  uniqs  7378  rankcf  9153  dprd2da  17618  t1ficld  20285  discmp  20355  xkoinjcn  20644  metnrmlem2  21819  metnrmlem2OLD  21834  ovoliunlem1  22397  i1fima  22578  i1fd  22581  itg1addlem5  22600  sibfof  29125  bnj1415  29799  cvmlift2lem12  29989  dftrpred4g  30426  poimirlem30  31877  itg2addnclem2  31901  ftc1anclem6  31929