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

Proof

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