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 1541	. . . 4 class 𝑥
5	4, 1	wceq 1542	. . 3 wff 𝑥 = 𝐴
6	5, 3	cab 2710	. 2 class {𝑥 ∣ 𝑥 = 𝐴}
7	2, 6	wceq 1542	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  6967  suppvalbr  8145  snec  8770  fset0  8844  0map0sn0  8875  infmap2  10209  cf0  10242  cflecard  10244  brdom7disj  10522  brdom6disj  10523  vdwlem6  16915  hashbc0  16934  symgbas0  19249  psrbagsn  21606  ptcmplem2  23539  snclseqg  23602  nmoo0  30022  nmop0  31217  nmfn0  31218  disjabrex  31791  disjabrexf  31792  pstmfval  32814  hasheuni  33021  derang0  34098  dfiota3  34833  bj-nuliotaALT  35877  poimirlem28  36454  lineset  38547  abbi1sn  40988  frege54cor1c  42599  iotain  43109  csbsngVD  43587  dfaimafn2  45809  dfatsnafv2  45895  rnfdmpr  45924