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

Definition df-sn 3334
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 3342. (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 3328 . 2 class {A}
3 vx . . . . 5 setvar x
43cv 1373 . . . 4 class x
54, 1wceq 1374 . . 3 wff x = A
65, 3cab 2009 . 2 class {xx = A}
72, 6wceq 1374 1 wff {A} = {xx = A}
Colors of variables: wff set class
This definition is referenced by:  sneq  3339  elsn  3343  elsncg  3350  csbsng  3383  rabsn  3389  pw0  3463  iunid  3665  dfiota2  4772  uniabio  4781  dfimafn2  5125  fnsnfv  5134  snec  6049
  Copyright terms: Public domain W3C validator