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 4211
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 4223. (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 4210 . 2 class {𝐴}
3 vx . . . . 5 setvar 𝑥
43cv 1522 . . . 4 class 𝑥
54, 1wceq 1523 . . 3 wff 𝑥 = 𝐴
65, 3cab 2637 . 2 class {𝑥𝑥 = 𝐴}
72, 6wceq 1523 1 wff {𝐴} = {𝑥𝑥 = 𝐴}
Colors of variables: wff setvar class
This definition is referenced by:  sneq  4220  elsng  4224  rabeqsn  4246  rabsssn  4247  csbsng  4275  rabsn  4288  pw0  4375  iunid  4607  dfiota2  5890  uniabio  5899  dfimafn2  6285  fnsnfv  6297  suppvalbr  7344  snec  7853  infmap2  9078  cf0  9111  cflecard  9113  brdom7disj  9391  brdom6disj  9392  vdwlem6  15737  hashbc0  15756  symgbas0  17860  psrbagsn  19543  ptcmplem2  21904  snclseqg  21966  nmoo0  27774  nmop0  28973  nmfn0  28974  disjabrex  29521  disjabrexf  29522  pstmfval  30067  hasheuni  30275  derang0  31277  dfiota3  32155  bj-nuliotaALT  33145  poimirlem28  33567  lineset  35342  frege54cor1c  38526  iotain  38935  csbsngVD  39443  dfaimafn2  41567  rnfdmpr  41623
  Copyright terms: Public domain W3C validator