ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  df-sn Structured version   GIF 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 {A} = {xx = A}
Distinct variable group:   x,A

Detailed syntax breakdown of Definition df-sn
StepHypRef Expression
1 cA . . 3 class A
21csn 3367 . 2 class {A}
3 vx . . . . 5 setvar x
43cv 1241 . . . 4 class x
54, 1wceq 1242 . . 3 wff x = A
65, 3cab 2023 . 2 class {xx = A}
72, 6wceq 1242 1 wff {A} = {xx = A}
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  9259
  Copyright terms: Public domain W3C validator