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

Definition df-sn 3356
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 3364. (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 3350 . 2 class {A}
3 vx . . . . 5 setvar x
43cv 1227 . . . 4 class x
54, 1wceq 1228 . . 3 wff x = A
65, 3cab 2008 . 2 class {xx = A}
72, 6wceq 1228 1 wff {A} = {xx = A}
Colors of variables: wff set class
This definition is referenced by:  sneq  3361  elsn  3365  elsncg  3372  csbsng  3405  rabsn  3411  pw0  3485  iunid  3686  dfiota2  4795  uniabio  4804  dfimafn2  5148  fnsnfv  5157  snec  6078  bdcsn  7097
  Copyright terms: Public domain W3C validator