Definition df-sn 4574

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 4667. For an alternate definition see dfsn2 4586. (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 4573	. 2 class {𝐴}
3		vx	. . . . 5 setvar 𝑥
4	3	cv 1540	. . . 4 class 𝑥
5	4, 1	wceq 1541	. . 3 wff 𝑥 = 𝐴
6	5, 3	cab 2709	. 2 class {𝑥 ∣ 𝑥 = 𝐴}
7	2, 6	wceq 1541	1 wff {𝐴} = {𝑥 ∣ 𝑥 = 𝐴}

This definition is referenced by:  sneq  4583  elsng  4587  absn  4593  dfsn2ALT  4595  rabsssn  4618  csbsng  4658  pw0  4761  uniabio  6451  iotaval  6455  dfimafn2  6885  suppvalbr  8094  snec  8702  fset0  8778  0map0sn0  8809  infmap2  10108  cf0  10142  cflecard  10144  brdom7disj  10422  brdom6disj  10423  vdwlem6  16898  hashbc0  16917  symgbas0  19301  pzriprnglem10  21427  pzriprnglem11  21428  psrbagsn  21998  ptcmplem2  23968  snclseqg  24031  1p1e2s  28339  twocut  28346  halfcut  28378  pw2cut2  28382  nmoo0  30771  nmop0  31966  nmfn0  31967  disjabrex  32562  disjabrexf  32563  pstmfval  33909  hasheuni  34098  derang0  35213  dfiota3  35965  bj-nuliotaALT  37102  poimirlem28  37698  dmcnvep  38422  lineset  39847  abbi1sn  42326  absnw  42781  frege54cor1c  44018  iotain  44520  csbsngVD  44995  dfaimafn2  47276  dfatsnafv2  47362  rnfdmpr  47391  stgr1  48071