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

This definition is used by:  sneq  4598  elsng  4602  absn  4608  dfsn2ALT  4610  rabsssn  4633  csbsng  4673  pw0  4777  moabex  5438  uniabio  6506  iotaval  6510  dfimafn2  6944  suppvalbr  8158  snecg  8773  snec  8774  fset0  8849  0map0sn0  8881  infmap2  10207  cf0  10240  cflecard  10242  brdom7disj  10521  brdom6disj  10522  vdwlem6  17052  hashbc0  17071  symgbas0  19465  pzriprnglem10  21651  pzriprnglem11  21652  psrbagsn  22225  ptcmplem2  24221  snclseqg  24284  twocut  28627  halfcut  28662  pw2cut2  28666  nmoo0  31154  nmop0  32349  nmfn0  32350  disjabrex  32938  disjabrexf  32939  pstmfval  34295  hasheuni  34484  derang0  35669  dfiota3  36421  bj-nuliotaALT  37722  poimirlem28  38327  dmcnvep  39065  ecqmap  39126  lineset  40540  abbi1sn  43022  absnw  43438  frege54cor1c  44669  iotain  45155  csbsngVD  45629  dfaimafn2  47931  dfatsnafv2  48017  rnfdmpr  48046  stgr1  48754