Definition df-sn 4178

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, although it is not very meaningful in this case. For an alternate definition see dfsn2 4190. (Contributed by NM, 21-Jun-1993.)

Assertion

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

Distinct variable group:   x, A

Detailed syntax breakdown of Definition df-sn

Step	Hyp	Ref	Expression
1		cA	. . 3 class A
2	1	csn 4177	. 2 class { A }
3		vx	. . . . 5 setvar x
4	3	cv 1482	. . . 4 class x
5	4, 1	wceq 1483	. . 3 wff x = A
6	5, 3	cab 2608	. 2 class { x | x = A }
7	2, 6	wceq 1483	1 wff { A } = { x | x = A }

This definition is referenced by:  sneq  4187  elsng  4191  rabeqsn  4214  rabsssn  4215  csbsng  4243  rabsn  4256  pw0  4343  iunid  4575  dfiota2  5852  uniabio  5861  dfimafn2  6246  fnsnfv  6258  suppvalbr  7299  snec  7810  infmap2  9040  cf0  9073  cflecard  9075  brdom7disj  9353  brdom6disj  9354  vdwlem6  15690  hashbc0  15709  symgbas0  17814  psrbagsn  19495  ptcmplem2  21857  snclseqg  21919  nmoo0  27646  nmop0  28845  nmfn0  28846  disjabrex  29395  disjabrexf  29396  pstmfval  29939  hasheuni  30147  derang0  31151  dfiota3  32030  bj-nuliotaALT  33020  poimirlem28  33437  lineset  35024  frege54cor1c  38209  iotain  38618  csbsngVD  39129  dfaimafn2  41246  rnfdmpr  41300