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

Definition df-sn 3844
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 3852. (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 3838 . 2  class  { A }
3 vx . . . . 5  set  x
43cv 1652 . . . 4  class  x
54, 1wceq 1653 . . 3  wff  x  =  A
65, 3cab 2428 . 2  class  { x  |  x  =  A }
72, 6wceq 1653 1  wff  { A }  =  { x  |  x  =  A }
Colors of variables: wff set class
This definition is referenced by:  sneq  3849  elsn  3853  elsncg  3860  csbsng  3891  rabsn  3897  pw0  3969  iunid  4170  dfiota2  5448  uniabio  5457  dfimafn2  5805  fnsnfv  5815  snec  6996  infmap2  8129  cf0  8162  cflecard  8164  brdom7disj  8440  brdom6disj  8441  vdwlem6  13385  hashbc0  13404  psrbagsn  16586  ptcmplem2  18115  snclseqg  18176  nmoo0  22323  nmop0  23520  nmfn0  23521  disjabrex  24055  disjabrexf  24056  pstmfval  24322  hasheuni  24506  derang0  24886  dfiota3  25799  uvcff  27255  iotain  27632  dfaimafn2  28044  rnfdmpr  28125  csbsngVD  29103  lineset  30633
  Copyright terms: Public domain W3C validator