Definition df-sn 4589

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 4682. For an alternate definition see dfsn2 4601. (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 4588	. 2 class {𝐴}
3		vx	. . . . 5 setvar 𝑥
4	3	cv 1567	. . . 4 class 𝑥
5	4, 1	wceq 1568	. . 3 wff 𝑥 = 𝐴
6	5, 3	cab 2739	. 2 class {𝑥 ∣ 𝑥 = 𝐴}
7	2, 6	wceq 1568	1 wff {𝐴} = {𝑥 ∣ 𝑥 = 𝐴}

This definition is referenced by:  sneq  4598  elsng  4602  absn  4608  dfsn2ALT  4610  rabsssn  4633  csbsng  4673  pw0  4777  moabex  5439  uniabio  6506  iotaval  6510  dfimafn2  6944  suppvalbr  8159  snecg  8774  snec  8775  fset0  8850  0map0sn0  8882  infmap2  10199  cf0  10233  cflecard  10235  brdom7disj  10514  brdom6disj  10515  vdwlem6  17045  hashbc0  17064  symgbas0  19458  pzriprnglem10  21619  pzriprnglem11  21620  psrbagsn  22193  ptcmplem2  24189  snclseqg  24252  twocut  28592  halfcut  28627  pw2cut2  28631  nmoo0  31109  nmop0  32304  nmfn0  32305  disjabrex  32893  disjabrexf  32894  pstmfval  34252  hasheuni  34441  derang0  35615  dfiota3  36367  bj-nuliotaALT  37638  poimirlem28  38243  dmcnvep  38983  ecqmap  39044  lineset  40458  abbi1sn  42940  absnw  43358  frege54cor1c  44589  iotain  45075  csbsngVD  45549  dfaimafn2  47848  dfatsnafv2  47934  rnfdmpr  47963  stgr1  48671