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 4156
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 4168. (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 4155 . 2 class {𝐴}
3 vx . . . . 5 setvar 𝑥
43cv 1479 . . . 4 class 𝑥
54, 1wceq 1480 . . 3 wff 𝑥 = 𝐴
65, 3cab 2607 . 2 class {𝑥𝑥 = 𝐴}
72, 6wceq 1480 1 wff {𝐴} = {𝑥𝑥 = 𝐴}
Colors of variables: wff setvar class
This definition is referenced by:  sneq  4165  elsng  4169  rabeqsn  4192  rabsssn  4193  csbsng  4221  rabsn  4233  pw0  4318  iunid  4548  dfiota2  5821  uniabio  5830  dfimafn2  6213  fnsnfv  6225  suppvalbr  7259  snec  7770  infmap2  9000  cf0  9033  cflecard  9035  brdom7disj  9313  brdom6disj  9314  vdwlem6  15633  hashbc0  15652  symgbas0  17754  psrbagsn  19435  ptcmplem2  21797  snclseqg  21859  nmoo0  27534  nmop0  28733  nmfn0  28734  disjabrex  29281  disjabrexf  29282  pstmfval  29763  hasheuni  29970  derang0  30912  dfiota3  31725  bj-nuliotaALT  32720  poimirlem28  33108  lineset  34543  frege54cor1c  37730  iotain  38139  csbsngVD  38651  dfaimafn2  40580  rnfdmpr  40627
  Copyright terms: Public domain W3C validator