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

Metamath Proof Explorer

Theorem unisng

Description: A set equals the union of its singleton. Theorem 8.2 of Quine p. 53. (Contributed by NM, 13-Aug-2002)

		Ref	Expression
	Assertion	unisng	$⊢ A \in V \to ⋃ \{A\} = A$

Step	Hyp	Ref	Expression
1		dfsn2	$⊢ \{A\} = \{A, A\}$
2	1	unieqi	$⊢ ⋃ \{A\} = ⋃ \{A, A\}$
3	2	a1i	$⊢ A \in V \to ⋃ \{A\} = ⋃ \{A, A\}$
4		uniprg	$⊢ (A \in V \land A \in V) \to ⋃ \{A, A\} = A \cup A$
5	4	anidms	$⊢ A \in V \to ⋃ \{A, A\} = A \cup A$
6		unidm	$⊢ A \cup A = A$
7	6	a1i	$⊢ A \in V \to A \cup A = A$
8	3 5 7	3eqtrd	$⊢ A \in V \to ⋃ \{A\} = A$