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 4562
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 4653. For an alternate definition see dfsn2 4574. (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 4561 . 2 class {𝐴}
3 vx . . . . 5 setvar 𝑥
43cv 1538 . . . 4 class 𝑥
54, 1wceq 1539 . . 3 wff 𝑥 = 𝐴
65, 3cab 2715 . 2 class {𝑥𝑥 = 𝐴}
72, 6wceq 1539 1 wff {𝐴} = {𝑥𝑥 = 𝐴}
Colors of variables: wff setvar class
This definition is referenced by:  sneq  4571  elsng  4575  absn  4579  dfsn2ALT  4581  rabsssn  4603  csbsng  4644  pw0  4745  iunid  4990  uniabio  6406  dfimafn2  6833  fnsnfvOLD  6848  suppvalbr  7981  snec  8569  fset0  8642  0map0sn0  8673  infmap2  9974  cf0  10007  cflecard  10009  brdom7disj  10287  brdom6disj  10288  vdwlem6  16687  hashbc0  16706  symgbas0  18996  psrbagsn  21271  ptcmplem2  23204  snclseqg  23267  nmoo0  29153  nmop0  30348  nmfn0  30349  disjabrex  30921  disjabrexf  30922  pstmfval  31846  hasheuni  32053  derang0  33131  dfiota3  34225  bj-nuliotaALT  35229  poimirlem28  35805  lineset  37752  abbi1sn  40191  frege54cor1c  41523  iotain  42035  csbsngVD  42513  dfaimafn2  44658  dfatsnafv2  44744  rnfdmpr  44773
  Copyright terms: Public domain W3C validator