This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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	$⊢ ⋃_{x \in A} \{x\} = A$

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