Definition df-sn 4590

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 4681. For an alternate definition see dfsn2 4602. (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 4589	. 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  4599  elsng  4603  absn  4609  dfsn2ALT  4611  rabsssn  4632  csbsng  4672  pw0  4776  iunidOLD  5025  uniabio  6478  iotaval  6482  dfimafn2  6924  suppvalbr  8143  snec  8751  fset0  8827  0map0sn0  8858  infmap2  10170  cf0  10204  cflecard  10206  brdom7disj  10484  brdom6disj  10485  vdwlem6  16957  hashbc0  16976  symgbas0  19319  pzriprnglem10  21400  pzriprnglem11  21401  psrbagsn  21970  ptcmplem2  23940  snclseqg  24003  1p1e2s  28302  twocut  28309  halfcut  28333  nmoo0  30720  nmop0  31915  nmfn0  31916  disjabrex  32511  disjabrexf  32512  pstmfval  33886  hasheuni  34075  derang0  35156  dfiota3  35911  bj-nuliotaALT  37046  poimirlem28  37642  dmcnvep  38361  lineset  39732  abbi1sn  42211  absnw  42666  frege54cor1c  43904  iotain  44406  csbsngVD  44882  dfaimafn2  47167  dfatsnafv2  47253  rnfdmpr  47282  stgr1  47960