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 e. V -> U. { A } = A )

Proof

Step	Hyp	Ref	Expression
1		dfsn2	|- { A } = { A , A }
2	1	unieqi	|- U. { A } = U. { A , A }
3	2	a1i	|- ( A e. V -> U. { A } = U. { A , A } )
4		uniprg	|- ( ( A e. V /\ A e. V ) -> U. { A , A } = ( A u. A ) )
5	4	anidms	|- ( A e. V -> U. { A , A } = ( A u. A ) )
6		unidm	|- ( A u. A ) = A
7	6	a1i	|- ( A e. V -> ( A u. A ) = A )
8	3 5 7	3eqtrd	|- ( A e. V -> U. { A } = A )