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

Metamath Proof Explorer

Theorem snid

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

Ref Expression
Hypothesis snid.1 ⊢ A ∈ V
Assertion snid ⊢ A ∈ A

Proof

Step Hyp Ref Expression
1 snid.1 ⊢ A ∈ V
2 snidb ⊢ A ∈ V ↔ A ∈ A
3 1 2 mpbi ⊢ A ∈ A