Metamath Proof Explorer


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 V
Assertion unisn A = A

Proof

Step Hyp Ref Expression
1 unisn.1 A V
2 unisng A V A = A
3 1 2 ax-mp A = A