Definition df-sn 4558

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 4651. For an alternate definition see dfsn2 4570. (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 4557	. 2 class {𝐴}
3		vx	. . . . 5 setvar 𝑥
4	3	cv 1541	. . . 4 class 𝑥
5	4, 1	wceq 1542	. . 3 wff 𝑥 = 𝐴
6	5, 3	cab 2713	. 2 class {𝑥 ∣ 𝑥 = 𝐴}
7	2, 6	wceq 1542	1 wff {𝐴} = {𝑥 ∣ 𝑥 = 𝐴}

This definition is referenced by:  sneq  4567  elsng  4571  absn  4577  dfsn2ALT  4579  rabsssn  4602  csbsng  4642  pw0  4745  moabex  5399  uniabio  6457  iotaval  6461  dfimafn2  6892  suppvalbr  8103  snecg  8713  snec  8714  fset0  8790  0map0sn0  8822  infmap2  10128  cf0  10162  cflecard  10164  brdom7disj  10442  brdom6disj  10443  vdwlem6  16946  hashbc0  16965  symgbas0  19353  pzriprnglem10  21459  pzriprnglem11  21460  psrbagsn  22030  ptcmplem2  24006  snclseqg  24069  twocut  28403  halfcut  28438  pw2cut2  28442  nmoo0  30850  nmop0  32045  nmfn0  32046  disjabrex  32640  disjabrexf  32641  pstmfval  34028  hasheuni  34217  derang0  35339  dfiota3  36091  bj-nuliotaALT  37353  poimirlem28  37957  dmcnvep  38697  ecqmap  38758  lineset  40172  abbi1sn  42652  absnw  43099  frege54cor1c  44330  iotain  44832  csbsngVD  45307  dfaimafn2  47602  dfatsnafv2  47688  rnfdmpr  47717  stgr1  48425