MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-sn Unicode version

Definition df-sn 3812
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 3820. (Contributed by NM, 5-Aug-1993.)
Assertion
Ref Expression
df-sn  |-  { A }  =  { x  |  x  =  A }
Distinct variable group:    x, A

Detailed syntax breakdown of Definition df-sn
StepHypRef Expression
1 cA . . 3  class  A
21csn 3806 . 2  class  { A }
3 vx . . . . 5  set  x
43cv 1651 . . . 4  class  x
54, 1wceq 1652 . . 3  wff  x  =  A
65, 3cab 2421 . 2  class  { x  |  x  =  A }
72, 6wceq 1652 1  wff  { A }  =  { x  |  x  =  A }
Colors of variables: wff set class
This definition is referenced by:  sneq  3817  elsn  3821  elsncg  3828  csbsng  3859  rabsn  3865  pw0  3937  iunid  4138  dfiota2  5410  uniabio  5419  dfimafn2  5767  fnsnfv  5777  snec  6958  infmap2  8087  cf0  8120  cflecard  8122  brdom7disj  8398  brdom6disj  8399  vdwlem6  13342  hashbc0  13361  psrbagsn  16543  ptcmplem2  18072  snclseqg  18133  nmoo0  22280  nmop0  23477  nmfn0  23478  disjabrex  24012  disjabrexf  24013  pstmfval  24279  hasheuni  24463  derang0  24843  dfiota3  25718  uvcff  27155  iotain  27532  dfaimafn2  27944  rnfdmpr  28014  csbsngVD  28859  lineset  30374
  Copyright terms: Public domain W3C validator