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

Definition df-sn 3900
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 , although it is not very meaningful in this case. For an alternate definition see dfsn2 3908. (Contributed by NM, 5-Aug-1993.)
Assertion
Ref Expression
df-sn
Distinct variable group:   ,

Detailed syntax breakdown of Definition df-sn
StepHypRef Expression
1 cA . . 3
21csn 3894 . 2
3 vx . . . . 5
43cv 1661 . . . 4
54, 1wceq 1662 . . 3
65, 3cab 2467 . 2
72, 6wceq 1662 1
Colors of variables: wff set class
This definition is referenced by:  sneq  3905  elsn  3909  elsncg  3917  csbsng  3952  rabsn  3958  pw0  4030  iunid  4235  dfiota2  5381  uniabio  5390  dfimafn2  5734  fnsnfv  5744  snec  7079  infmap2  8212  cf0  8245  cflecard  8247  brdom7disj  8523  brdom6disj  8524  vdwlem6  13833  hashbc0  13852  psrbagsn  17058  ptcmplem2  18588  snclseqg  18649  nmoo0  22801  nmop0  24000  nmfn0  24001  disjabrex  24545  disjabrexf  24546  pstmfval  24993  hasheuni  25205  derang0  25694  dfiota3  26598  uvcff  28146  iotain  28520  dfaimafn2  28928  rnfdmpr  29008  csbsngVD  30198  lineset  31808
  Copyright terms: Public domain W3C validator