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

Definition df-sn 3503
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 3511. (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 3497 . 2 class {𝐴}
3 vx . . . . 5 setvar 𝑥
43cv 1315 . . . 4 class 𝑥
54, 1wceq 1316 . . 3 wff 𝑥 = 𝐴
65, 3cab 2103 . 2 class {𝑥𝑥 = 𝐴}
72, 6wceq 1316 1 wff {𝐴} = {𝑥𝑥 = 𝐴}
Colors of variables: wff set class
This definition is referenced by:  sneq  3508  elsng  3512  csbsng  3554  rabsn  3560  pw0  3637  iunid  3838  dfiota2  5059  uniabio  5068  dfimafn2  5439  fnsnfv  5448  snec  6458  bdcsn  12964
  Copyright terms: Public domain W3C validator