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.

Step	Hyp	Ref	Expression
1		df-sn 3960	. . . . 5 |- { x } = { y | y = x }
2		equcom 1870	. . . . . 6 |- ( y = x <-> x = y )
3	2	abbii 2587	. . . . 5 |- { y | y = x } = { y | x = y }
4	1, 3	eqtri 2493	. . . 4 |- { x } = { y | x = y }
5	4	a1i 11	. . 3 |- ( x e. A -> { x } = { y | x = y } )
6	5	iuneq2i 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 )
9	8	abbii 2587	. . 3 |- { y | y e. A } = { y | E. x e. A x = y }
10		abid2 2593	. . 3 |- { y | y e. A } = A
11	7, 9, 10	3eqtr2i 2499	. 2 |- U_ x e. A { y | x = y } = A
12	6, 11	eqtri 2493	1 |- U_ x e. A { x } = A

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