This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ∈ V → A ∈ A

Proof

Step Hyp Ref Expression
1 eqid ⊢ A = A
2 elsng ⊢ A ∈ V → A ∈ A ↔ A = A
3 1 2 mpbiri ⊢ A ∈ V → A ∈ A