Definition df-sn 4632

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 4722. For an alternate definition see dfsn2 4644. (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 4631	. 2 class {𝐴}
3		vx	. . . . 5 setvar 𝑥
4	3	cv 1536	. . . 4 class 𝑥
5	4, 1	wceq 1537	. . 3 wff 𝑥 = 𝐴
6	5, 3	cab 2712	. 2 class {𝑥 ∣ 𝑥 = 𝐴}
7	2, 6	wceq 1537	1 wff {𝐴} = {𝑥 ∣ 𝑥 = 𝐴}

This definition is referenced by:  sneq  4641  elsng  4645  absn  4650  dfsn2ALT  4652  rabsssn  4673  csbsng  4713  pw0  4817  iunidOLD  5066  uniabio  6530  iotaval  6534  dfimafn2  6972  suppvalbr  8188  snec  8819  fset0  8893  0map0sn0  8924  infmap2  10255  cf0  10289  cflecard  10291  brdom7disj  10569  brdom6disj  10570  vdwlem6  17020  hashbc0  17039  symgbas0  19421  pzriprnglem10  21519  pzriprnglem11  21520  psrbagsn  22105  ptcmplem2  24077  snclseqg  24140  1p1e2s  28415  nohalf  28422  halfcut  28431  nmoo0  30820  nmop0  32015  nmfn0  32016  disjabrex  32602  disjabrexf  32603  pstmfval  33857  hasheuni  34066  derang0  35154  dfiota3  35905  bj-nuliotaALT  37041  poimirlem28  37635  lineset  39721  abbi1sn  42241  absnw  42665  frege54cor1c  43905  iotain  44413  csbsngVD  44891  dfaimafn2  47116  dfatsnafv2  47202  rnfdmpr  47231  stgr1  47864