Theorem unisn

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

	Ref	Expression
Hypothesis	unisn.1	|- A e. _V
Assertion	unisn	|- U. { A } = A

Proof

Step	Hyp	Ref	Expression
1		unisn.1	|- A e. _V
2		unisng	|- ( A e. _V -> U. { A } = A )
3	1 2	ax-mp	|- U. { A } = A