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

Proof

Step Hyp Ref Expression
1 eqid 
 |-  A = A
2 elsng 
 |-  ( A e. V -> ( A e. { A } <-> A = A ) )
3 1 2 mpbiri 
 |-  ( A e. V -> A e. { A } )