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 4560
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 4647. For an alternate definition see dfsn2 4572. (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 4559 . 2 class {𝐴}
3 vx . . . . 5 setvar 𝑥
43cv 1527 . . . 4 class 𝑥
54, 1wceq 1528 . . 3 wff 𝑥 = 𝐴
65, 3cab 2799 . 2 class {𝑥𝑥 = 𝐴}
72, 6wceq 1528 1 wff {𝐴} = {𝑥𝑥 = 𝐴}
Colors of variables: wff setvar class
This definition is referenced by:  sneq  4569  elsng  4573  absn  4577  dfsn2ALT  4579  rabsssn  4599  csbsng  4638  pw0  4739  iunid  4976  uniabio  6322  dfimafn2  6723  fnsnfv  6737  suppvalbr  7825  snec  8350  infmap2  9629  cf0  9662  cflecard  9664  brdom7disj  9942  brdom6disj  9943  vdwlem6  16312  hashbc0  16331  symgbas0  18453  psrbagsn  20205  ptcmplem2  22591  snclseqg  22653  nmoo0  28496  nmop0  29691  nmfn0  29692  disjabrex  30261  disjabrexf  30262  pstmfval  31036  hasheuni  31244  derang0  32314  dfiota3  33282  bj-nuliotaALT  34246  poimirlem28  34802  lineset  36756  frege54cor1c  40141  iotain  40629  csbsngVD  41107  dfaimafn2  43246  dfatsnafv2  43332  rnfdmpr  43361  efmndbas0  43958
  Copyright terms: Public domain W3C validator