Definition df-sn 4582

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 4675. For an alternate definition see dfsn2 4594. (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 4581	. 2 class {𝐴}
3		vx	. . . . 5 setvar 𝑥
4	3	cv 1541	. . . 4 class 𝑥
5	4, 1	wceq 1542	. . 3 wff 𝑥 = 𝐴
6	5, 3	cab 2715	. 2 class {𝑥 ∣ 𝑥 = 𝐴}
7	2, 6	wceq 1542	1 wff {𝐴} = {𝑥 ∣ 𝑥 = 𝐴}

This definition is referenced by:  sneq  4591  elsng  4595  absn  4601  dfsn2ALT  4603  rabsssn  4626  csbsng  4666  pw0  4769  moabex  5407  uniabio  6463  iotaval  6467  dfimafn2  6898  suppvalbr  8108  snecg  8718  snec  8719  fset0  8795  0map0sn0  8827  infmap2  10131  cf0  10165  cflecard  10167  brdom7disj  10445  brdom6disj  10446  vdwlem6  16918  hashbc0  16937  symgbas0  19322  pzriprnglem10  21449  pzriprnglem11  21450  psrbagsn  22022  ptcmplem2  24001  snclseqg  24064  twocut  28423  halfcut  28458  pw2cut2  28462  nmoo0  30870  nmop0  32065  nmfn0  32066  disjabrex  32660  disjabrexf  32661  pstmfval  34055  hasheuni  34244  derang0  35365  dfiota3  36117  bj-nuliotaALT  37261  poimirlem28  37851  dmcnvep  38591  ecqmap  38652  lineset  40066  abbi1sn  42547  absnw  42988  frege54cor1c  44223  iotain  44725  csbsngVD  45200  dfaimafn2  47479  dfatsnafv2  47565  rnfdmpr  47594  stgr1  48274