Definition df-sn 4580

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 4671. For an alternate definition see dfsn2 4592. (Contributed by NM, 21-Jun-1993.)

Assertion

Ref	Expression
df-sn	⊢ {𝐴} = {𝑥 ∣ 𝑥 = 𝐴}

Distinct variable group:   𝑥,𝐴

Detailed syntax breakdown of Definition df-sn

Step	Hyp	Ref	Expression
1		cA	. . 3 class 𝐴
2	1	csn 4579	. 2 class {𝐴}
3		vx	. . . . 5 setvar 𝑥
4	3	cv 1539	. . . 4 class 𝑥
5	4, 1	wceq 1540	. . 3 wff 𝑥 = 𝐴
6	5, 3	cab 2707	. 2 class {𝑥 ∣ 𝑥 = 𝐴}
7	2, 6	wceq 1540	1 wff {𝐴} = {𝑥 ∣ 𝑥 = 𝐴}

This definition is referenced by:  sneq  4589  elsng  4593  absn  4599  dfsn2ALT  4601  rabsssn  4622  csbsng  4662  pw0  4766  iunidOLD  5013  uniabio  6456  iotaval  6460  dfimafn2  6890  suppvalbr  8104  snec  8712  fset0  8788  0map0sn0  8819  infmap2  10130  cf0  10164  cflecard  10166  brdom7disj  10444  brdom6disj  10445  vdwlem6  16917  hashbc0  16936  symgbas0  19287  pzriprnglem10  21416  pzriprnglem11  21417  psrbagsn  21987  ptcmplem2  23957  snclseqg  24020  1p1e2s  28327  twocut  28334  halfcut  28365  nmoo0  30754  nmop0  31949  nmfn0  31950  disjabrex  32545  disjabrexf  32546  pstmfval  33882  hasheuni  34071  derang0  35161  dfiota3  35916  bj-nuliotaALT  37051  poimirlem28  37647  dmcnvep  38366  lineset  39737  abbi1sn  42216  absnw  42671  frege54cor1c  43908  iotain  44410  csbsngVD  44886  dfaimafn2  47170  dfatsnafv2  47256  rnfdmpr  47285  stgr1  47965