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

Metamath Proof Explorer

Theorem snex

Description: A singleton is a set. Theorem 7.12 of Quine p. 51, proved using Extensionality, Separation and Pairing. See also snexALT . (Contributed by NM, 7-Aug-1994) (Revised by Mario Carneiro, 19-May-2013) Avoid ax-nul and shorten proof. (Revised by GG, 6-Mar-2026)

Ref Expression
Assertion snex ⊢ A ∈ V

Proof

Step Hyp Ref Expression
1 dfsn2 ⊢ A = A A
2 prex ⊢ A A ∈ V
3 1 2 eqeltri ⊢ A ∈ V