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

Definition df-sn 3537
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 3545. (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 class 𝐴
21csn 3531 . 2 class {𝐴}
3 vx . . . . 5 setvar 𝑥
43cv 1331 . . . 4 class 𝑥
54, 1wceq 1332 . . 3 wff 𝑥 = 𝐴
65, 3cab 2126 . 2 class {𝑥𝑥 = 𝐴}
72, 6wceq 1332 1 wff {𝐴} = {𝑥𝑥 = 𝐴}
Colors of variables: wff set class
This definition is referenced by:  sneq  3542  elsng  3546  csbsng  3591  rabsn  3597  pw0  3674  iunid  3875  dfiota2  5096  uniabio  5105  dfimafn2  5478  fnsnfv  5487  snec  6497  bdcsn  13237
  Copyright terms: Public domain W3C validator