Theorem iunid

Description: An indexed union of singletons recovers the index set. (Contributed by NM, 6-Sep-2005) (Proof shortened by SN, 15-Jan-2025)

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

Proof

Step	Hyp	Ref	Expression
1		df-iun	$$⊢\bigcup _{x\in A}\left\{x\right\}=\left\{y|\exists x\in Ay\in \left\{x\right\}\right\}$$
2		clel5	$$⊢y\in A\leftrightarrow \exists x\in Ay=x$$
3		velsn	$$⊢y\in \left\{x\right\}\leftrightarrow y=x$$
4	3	rexbii	$$⊢\exists x\in Ay\in \left\{x\right\}\leftrightarrow \exists x\in Ay=x$$
5	2 4	bitr4i	$$⊢y\in A\leftrightarrow \exists x\in Ay\in \left\{x\right\}$$
6	5	eqabi	$$⊢A=\left\{y|\exists x\in Ay\in \left\{x\right\}\right\}$$
7	1 6	eqtr4i	$$⊢\bigcup _{x\in A}\left\{x\right\}=A$$