MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-sn Structured version   Visualization version   GIF version

Definition df-sn 4126
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 4138. (Contributed by NM, 21-Jun-1993.)
Assertion
Ref Expression
df-sn {𝐴} = {𝑥𝑥 = 𝐴}
Distinct variable group:   𝑥,𝐴

Detailed syntax breakdown of Definition df-sn
StepHypRef Expression
1 cA . . 3 class 𝐴
21csn 4125 . 2 class {𝐴}
3 vx . . . . 5 setvar 𝑥
43cv 1474 . . . 4 class 𝑥
54, 1wceq 1475 . . 3 wff 𝑥 = 𝐴
65, 3cab 2596 . 2 class {𝑥𝑥 = 𝐴}
72, 6wceq 1475 1 wff {𝐴} = {𝑥𝑥 = 𝐴}
Colors of variables: wff setvar class
This definition is referenced by:  sneq  4135  elsng  4139  rabeqsn  4161  rabsssn  4162  csbsng  4190  rabsn  4200  pw0  4283  iunid  4511  dfiota2  5769  uniabio  5778  dfimafn2  6156  fnsnfv  6168  suppvalbr  7186  snec  7697  infmap2  8923  cf0  8956  cflecard  8958  brdom7disj  9234  brdom6disj  9235  vdwlem6  15528  hashbc0  15547  symgbas0  17637  psrbagsn  19316  ptcmplem2  21667  snclseqg  21729  nmoo0  27030  nmop0  28229  nmfn0  28230  disjabrex  28777  disjabrexf  28778  pstmfval  29267  hasheuni  29474  derang0  30405  dfiota3  31200  bj-nuliotaALT  32211  poimirlem28  32607  lineset  34042  frege54cor1c  37229  iotain  37640  csbsngVD  38151  dfaimafn2  39895  rnfdmpr  40325
  Copyright terms: Public domain W3C validator