Theorem iunid

Description: An indexed union of singletons recovers the index set. (Contributed by NM, 6-Sep-2005)

	Ref	Expression
Assertion	iunid	|- U_ x e. A { x } = A

Proof

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