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

Definition df-sn 3346
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 3354. (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 3340 . 2 class {A}
3 vx . . . . 5 setvar x
43cv 1223 . . . 4 class x
54, 1wceq 1224 . . 3 wff x = A
65, 3cab 2000 . 2 class {xx = A}
72, 6wceq 1224 1 wff {A} = {xx = A}
Colors of variables: wff set class
This definition is referenced by:  sneq  3351  elsn  3355  elsncg  3362  csbsng  3395  rabsn  3401  pw0  3475  iunid  3676  dfiota2  4784  uniabio  4793  dfimafn2  5137  fnsnfv  5146  snec  6067  bdcsn  8327
  Copyright terms: Public domain W3C validator