Metamath Proof Explorer


Theorem snidg

Description: A set is a member of its singleton. Part of Theorem 7.6 of Quine p. 49. (Contributed by NM, 28-Oct-2003)

Ref Expression
Assertion snidg AVAA

Proof

Step Hyp Ref Expression
1 eqid A=A
2 elsng AVAAA=A
3 1 2 mpbiri AVAA