Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > df-sn | GIF version |
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 3541. (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
df-sn | ⊢ {𝐴} = {𝑥 ∣ 𝑥 = 𝐴} |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cA | . . 3 class 𝐴 | |
2 | 1 | csn 3527 | . 2 class {𝐴} |
3 | vx | . . . . 5 setvar 𝑥 | |
4 | 3 | cv 1330 | . . . 4 class 𝑥 |
5 | 4, 1 | wceq 1331 | . . 3 wff 𝑥 = 𝐴 |
6 | 5, 3 | cab 2125 | . 2 class {𝑥 ∣ 𝑥 = 𝐴} |
7 | 2, 6 | wceq 1331 | 1 wff {𝐴} = {𝑥 ∣ 𝑥 = 𝐴} |
Colors of variables: wff set class |
This definition is referenced by: sneq 3538 elsng 3542 csbsng 3584 rabsn 3590 pw0 3667 iunid 3868 dfiota2 5089 uniabio 5098 dfimafn2 5471 fnsnfv 5480 snec 6490 bdcsn 13068 |
Copyright terms: Public domain | W3C validator |