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 4314
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 4389. For an alternate definition see dfsn2 4326. (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 4313 . 2 class {𝐴}
3 vx . . . . 5 setvar 𝑥
43cv 1623 . . . 4 class 𝑥
54, 1wceq 1624 . . 3 wff 𝑥 = 𝐴
65, 3cab 2738 . 2 class {𝑥𝑥 = 𝐴}
72, 6wceq 1624 1 wff {𝐴} = {𝑥𝑥 = 𝐴}
Colors of variables: wff setvar class
This definition is referenced by:  sneq  4323  elsng  4327  dfsn2ALT  4332  rabeqsn  4350  rabsssn  4351  csbsng  4379  rabsn  4392  pw0  4480  iunid  4719  dfiota2  6005  uniabio  6014  dfimafn2  6400  fnsnfv  6412  suppvalbr  7459  snec  7969  infmap2  9224  cf0  9257  cflecard  9259  brdom7disj  9537  brdom6disj  9538  vdwlem6  15884  hashbc0  15903  symgbas0  18006  psrbagsn  19689  ptcmplem2  22050  snclseqg  22112  nmoo0  27947  nmop0  29146  nmfn0  29147  disjabrex  29694  disjabrexf  29695  pstmfval  30240  hasheuni  30448  derang0  31450  dfiota3  32328  bj-nuliotaALT  33318  poimirlem28  33742  lineset  35519  frege54cor1c  38703  iotain  39112  csbsngVD  39620  dfaimafn2  41744  rnfdmpr  41800
  Copyright terms: Public domain W3C validator