Definition df-sn 4579

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 4672. For an alternate definition see dfsn2 4591. (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 4578	. 2 class {𝐴}
3		vx	. . . . 5 setvar 𝑥
4	3	cv 1540	. . . 4 class 𝑥
5	4, 1	wceq 1541	. . 3 wff 𝑥 = 𝐴
6	5, 3	cab 2712	. 2 class {𝑥 ∣ 𝑥 = 𝐴}
7	2, 6	wceq 1541	1 wff {𝐴} = {𝑥 ∣ 𝑥 = 𝐴}

This definition is referenced by:  sneq  4588  elsng  4592  absn  4598  dfsn2ALT  4600  rabsssn  4623  csbsng  4663  pw0  4766  moabex  5404  uniabio  6460  iotaval  6464  dfimafn2  6895  suppvalbr  8104  snec  8713  fset0  8789  0map0sn0  8821  infmap2  10125  cf0  10159  cflecard  10161  brdom7disj  10439  brdom6disj  10440  vdwlem6  16912  hashbc0  16931  symgbas0  19316  pzriprnglem10  21443  pzriprnglem11  21444  psrbagsn  22016  ptcmplem2  23995  snclseqg  24058  1p1e2s  28374  twocut  28381  halfcut  28415  pw2cut2  28419  nmoo0  30815  nmop0  32010  nmfn0  32011  disjabrex  32606  disjabrexf  32607  pstmfval  34002  hasheuni  34191  derang0  35312  dfiota3  36064  bj-nuliotaALT  37202  poimirlem28  37788  dmcnvep  38512  lineset  39937  abbi1sn  42421  absnw  42863  frege54cor1c  44098  iotain  44600  csbsngVD  45075  dfaimafn2  47354  dfatsnafv2  47440  rnfdmpr  47469  stgr1  48149