Definition df-sn 4211

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, although it is not very meaningful in this case. For an alternate definition see dfsn2 4223. (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 4210	. 2 class {𝐴}
3		vx	. . . . 5 setvar 𝑥
4	3	cv 1522	. . . 4 class 𝑥
5	4, 1	wceq 1523	. . 3 wff 𝑥 = 𝐴
6	5, 3	cab 2637	. 2 class {𝑥 ∣ 𝑥 = 𝐴}
7	2, 6	wceq 1523	1 wff {𝐴} = {𝑥 ∣ 𝑥 = 𝐴}

This definition is referenced by:  sneq  4220  elsng  4224  rabeqsn  4246  rabsssn  4247  csbsng  4275  rabsn  4288  pw0  4375  iunid  4607  dfiota2  5890  uniabio  5899  dfimafn2  6285  fnsnfv  6297  suppvalbr  7344  snec  7853  infmap2  9078  cf0  9111  cflecard  9113  brdom7disj  9391  brdom6disj  9392  vdwlem6  15737  hashbc0  15756  symgbas0  17860  psrbagsn  19543  ptcmplem2  21904  snclseqg  21966  nmoo0  27774  nmop0  28973  nmfn0  28974  disjabrex  29521  disjabrexf  29522  pstmfval  30067  hasheuni  30275  derang0  31277  dfiota3  32155  bj-nuliotaALT  33145  poimirlem28  33567  lineset  35342  frege54cor1c  38526  iotain  38935  csbsngVD  39443  dfaimafn2  41567  rnfdmpr  41623