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 4125
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 4137. (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 4124 . 2 class {𝐴}
3 vx . . . . 5 setvar 𝑥
43cv 1473 . . . 4 class 𝑥
54, 1wceq 1474 . . 3 wff 𝑥 = 𝐴
65, 3cab 2595 . 2 class {𝑥𝑥 = 𝐴}
72, 6wceq 1474 1 wff {𝐴} = {𝑥𝑥 = 𝐴}
Colors of variables: wff setvar class
This definition is referenced by:  sneq  4134  elsng  4138  rabeqsn  4160  rabsssn  4161  csbsng  4189  rabsn  4199  pw0  4282  iunid  4505  dfiota2  5754  uniabio  5763  dfimafn2  6140  fnsnfv  6152  suppvalbr  7163  snec  7674  infmap2  8900  cf0  8933  cflecard  8935  brdom7disj  9211  brdom6disj  9212  vdwlem6  15476  hashbc0  15495  symgbas0  17585  psrbagsn  19264  ptcmplem2  21614  snclseqg  21676  nmoo0  26823  nmop0  28022  nmfn0  28023  disjabrex  28570  disjabrexf  28571  pstmfval  29060  hasheuni  29267  derang0  30198  dfiota3  30993  bj-nuliotaALT  31994  poimirlem28  32390  lineset  33825  frege54cor1c  37012  iotain  37423  csbsngVD  37934  dfaimafn2  39679  rnfdmpr  40120
  Copyright terms: Public domain W3C validator