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 1547	. . . 4 class 𝑥
5	4, 1	wceq 1548	. . 3 wff 𝑥 = 𝐴
6	5, 3	cab 2719	. 2 class {𝑥 ∣ 𝑥 = 𝐴}
7	2, 6	wceq 1548	1 wff {𝐴} = {𝑥 ∣ 𝑥 = 𝐴}

This definition is referenced by:  sneq  4567  elsng  4571  absn  4577  dfsn2ALT  4579  rabsssn  4602  csbsng  4642  pw0  4745  moabex  5399  uniabio  6458  iotaval  6462  dfimafn2  6893  suppvalbr  8106  snecg  8718  snec  8719  fset0  8795  0map0sn0  8827  infmap2  10134  cf0  10168  cflecard  10170  brdom7disj  10449  brdom6disj  10450  vdwlem6  16952  hashbc0  16971  symgbas0  19358  pzriprnglem10  21468  pzriprnglem11  21469  psrbagsn  22042  ptcmplem2  24039  snclseqg  24102  twocut  28435  halfcut  28470  pw2cut2  28474  nmoo0  30882  nmop0  32077  nmfn0  32078  disjabrex  32673  disjabrexf  32674  pstmfval  34090  hasheuni  34279  derang0  35410  dfiota3  36162  bj-nuliotaALT  37424  poimirlem28  38028  dmcnvep  38768  ecqmap  38829  lineset  40243  abbi1sn  42723  absnw  43141  frege54cor1c  44372  iotain  44874  csbsngVD  45349  dfaimafn2  47641  dfatsnafv2  47727  rnfdmpr  47756  stgr1  48464