Definition df-sn 4584

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 4677. For an alternate definition see dfsn2 4596. (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 4583	. 2 class {𝐴}
3		vx	. . . . 5 setvar 𝑥
4	3	cv 1568	. . . 4 class 𝑥
5	4, 1	wceq 1569	. . 3 wff 𝑥 = 𝐴
6	5, 3	cab 2738	. 2 class {𝑥 ∣ 𝑥 = 𝐴}
7	2, 6	wceq 1569	1 wff {𝐴} = {𝑥 ∣ 𝑥 = 𝐴}

This definition is used by:  sneq  4593  elsng  4597  absn  4603  dfsn2ALT  4605  rabsssn  4628  csbsng  4668  pw0  4772  moabex  5425  uniabio  6508  iotaval  6512  dfimafn2  6948  suppvalbr  8181  snecg  8798  snec  8799  fset0  8876  0map0sn0  8913  infmap2  10295  cf0  10328  cflecard  10330  brdom7disj  10610  brdom6disj  10611  vdwlem6  17164  hashbc0  17183  symgbas0  19603  pzriprnglem10  21796  pzriprnglem11  21797  psrbagsn  22372  ptcmplem2  24372  snclseqg  24435  twocut  28809  halfcut  28844  pw2cut2  28848  nmoo0  31393  nmop0  32588  nmfn0  32589  disjabrex  33218  disjabrexf  33219  pstmfval  34570  hasheuni  34759  derang0  35976  dfiota3  36727  bj-nuliotaALT  38015  poimirlem28  38609  dfproplem  38684  dmcnvep  39363  ecqmap  39424  lineset  40838  abbi1sn  43320  absnw  43732  frege54cor1c  44957  iotain  45443  csbsngVD  45917  dfaimafn2  48278  dfatsnafv2  48364  rnfdmpr  48393  stgr1  49101