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

Metamath Proof Explorer

Definition df-sn

Description: Define the singleton of a class. Definition 7.1 of Quine p. 48. For convenience, it is well-defined for proper classes, i.e., those that are not elements of _V , see snprc . For an alternate definition see dfsn2 . (Contributed by NM, 21-Jun-1993)

Ref Expression
Assertion df-sn 
|- { A } = { x | x = A }

Detailed syntax breakdown

Step Hyp Ref Expression
0 cA 
 |-  A
1 0 csn 
 |-  { A }
2 vx 
 |-  x
3 2 cv 
 |-  x
4 3 0 wceq 
 |-  x = A
5 4 2 cab 
 |-  { x | x = A }
6 1 5 wceq 
 |-  { A } = { x | x = A }