Definition df-sn 4628

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 4720. For an alternate definition see dfsn2 4640. (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 4627	. 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  4637  elsng  4641  absn  4645  dfsn2ALT  4647  rabsssn  4669  csbsng  4711  pw0  4814  iunidOLD  5063  uniabio  6507  iotaval  6511  dfimafn2  6952  fnsnfvOLD  6968  suppvalbr  8146  snec  8770  fset0  8844  0map0sn0  8875  infmap2  10209  cf0  10242  cflecard  10244  brdom7disj  10522  brdom6disj  10523  vdwlem6  16915  hashbc0  16934  symgbas0  19250  psrbagsn  21615  ptcmplem2  23548  snclseqg  23611  nmoo0  30031  nmop0  31226  nmfn0  31227  disjabrex  31800  disjabrexf  31801  pstmfval  32864  hasheuni  33071  derang0  34148  dfiota3  34883  bj-nuliotaALT  35927  poimirlem28  36504  lineset  38597  abbi1sn  41036  frege54cor1c  42651  iotain  43161  csbsngVD  43639  dfaimafn2  45860  dfatsnafv2  45946  rnfdmpr  45975