Theorem iunid

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

	Ref	Expression
Assertion	iunid	$$⊢\bigcup _{x\in A}\left\{x\right\}=A$$

Proof

Step	Hyp	Ref	Expression
1		df-sn	$$⊢\left\{x\right\}=\left\{y|y=x\right\}$$
2		equcom	$$⊢y=x\leftrightarrow x=y$$
3	2	abbii	$$⊢\left\{y|y=x\right\}=\left\{y|x=y\right\}$$
4	1 3	eqtri	$$⊢\left\{x\right\}=\left\{y|x=y\right\}$$
5	4	a1i	$$⊢x\in A\to \left\{x\right\}=\left\{y|x=y\right\}$$
6	5	iuneq2i	$$⊢\bigcup _{x\in A}\left\{x\right\}=\bigcup _{x\in A}\left\{y|x=y\right\}$$
7		iunab	$$⊢\bigcup _{x\in A}\left\{y|x=y\right\}=\left\{y|\exists x\in Ax=y\right\}$$
8		risset	$$⊢y\in A\leftrightarrow \exists x\in Ax=y$$
9	8	abbii	$$⊢\left\{y|y\in A\right\}=\left\{y|\exists x\in Ax=y\right\}$$
10		abid2	$$⊢\left\{y|y\in A\right\}=A$$
11	7 9 10	3eqtr2i	$$⊢\bigcup _{x\in A}\left\{y|x=y\right\}=A$$
12	6 11	eqtri	$$⊢\bigcup _{x\in A}\left\{x\right\}=A$$