ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  df-sn Structured version   Unicode version

Definition df-sn 3373
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 3381. (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 3367 . 2  { }
3 vx . . . . 5  setvar
43cv 1241 . . . 4
54, 1wceq 1242 . . 3
65, 3cab 2023 . 2  {  |  }
72, 6wceq 1242 1  { }  {  |  }
Colors of variables: wff set class
This definition is referenced by:  sneq  3378  elsn  3382  elsncg  3389  csbsng  3422  rabsn  3428  pw0  3502  iunid  3703  dfiota2  4811  uniabio  4820  dfimafn2  5166  fnsnfv  5175  snec  6103  bdcsn  9325
  Copyright terms: Public domain W3C validator