Theorem iunid 4373

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 4021	. . . . 5 |- { x } = { y | y = x }
2		equcom 1738	. . . . . 6 |- ( y = x <-> x = y )
3	2	abbii 2594	. . . . 5 |- { y | y = x } = { y | x = y }
4	1, 3	eqtri 2489	. . . 4 |- { x } = { y | x = y }
5	4	a1i 11	. . 3 |- ( x e. A -> { x } = { y | x = y } )
6	5	iuneq2i 4337	. 2 |- U_ x e. A { x } = U_ x e. A { y | x = y }
7		iunab 4364	. . 3 |- U_ x e. A { y | x = y } = { y | E. x e. A x = y }
8		risset 2980	. . . 4 |- ( y e. A <-> E. x e. A x = y )
9	8	abbii 2594	. . 3 |- { y | y e. A } = { y | E. x e. A x = y }
10		abid2 2600	. . 3 |- { y | y e. A } = A
11	7, 9, 10	3eqtr2i 2495	. 2 |- U_ x e. A { y | x = y } = A
12	6, 11	eqtri 2489	1 |- U_ x e. A { x } = A

Syntax hints:   = wceq 1374   e. wcel 1762   {cab 2445   E.wrex 2808   {csn 4020   U_ciun 4318

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1961  ax-ext 2438

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-clab 2446  df-cleq 2452  df-clel 2455  df-nfc 2610  df-ral 2812  df-rex 2813  df-v 3108  df-in 3476  df-ss 3483  df-sn 4021  df-iun 4320

This theorem is referenced by:  iunxpconst  5048  xpexgALT  6767  uniqs  7361  rankcf  9144  dprd2da  16874  t1ficld  19587  discmp  19657  xkoinjcn  19916  metnrmlem2  21092  ovoliunlem1  21641  i1fima  21813  i1fd  21816  itg1addlem5  21835  sibfof  27772  cvmlift2lem12  28249  dftrpred4g  28744  itg2addnclem2  29495  ftc1anclem6  29523  bnj1415  33048