Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > df-sn | Structured version Visualization version 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 4190. (Contributed by NM, 21-Jun-1993.) |
Ref | Expression |
---|---|
df-sn | ⊢ {𝐴} = {𝑥 ∣ 𝑥 = 𝐴} |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cA | . . 3 class 𝐴 | |
2 | 1 | csn 4177 | . 2 class {𝐴} |
3 | vx | . . . . 5 setvar 𝑥 | |
4 | 3 | cv 1482 | . . . 4 class 𝑥 |
5 | 4, 1 | wceq 1483 | . . 3 wff 𝑥 = 𝐴 |
6 | 5, 3 | cab 2608 | . 2 class {𝑥 ∣ 𝑥 = 𝐴} |
7 | 2, 6 | wceq 1483 | 1 wff {𝐴} = {𝑥 ∣ 𝑥 = 𝐴} |
Colors of variables: wff setvar class |
This definition is referenced by: sneq 4187 elsng 4191 rabeqsn 4214 rabsssn 4215 csbsng 4243 rabsn 4256 pw0 4343 iunid 4575 dfiota2 5852 uniabio 5861 dfimafn2 6246 fnsnfv 6258 suppvalbr 7299 snec 7810 infmap2 9040 cf0 9073 cflecard 9075 brdom7disj 9353 brdom6disj 9354 vdwlem6 15690 hashbc0 15709 symgbas0 17814 psrbagsn 19495 ptcmplem2 21857 snclseqg 21919 nmoo0 27646 nmop0 28845 nmfn0 28846 disjabrex 29395 disjabrexf 29396 pstmfval 29939 hasheuni 30147 derang0 31151 dfiota3 32030 bj-nuliotaALT 33020 poimirlem28 33437 lineset 35024 frege54cor1c 38209 iotain 38618 csbsngVD 39129 dfaimafn2 41246 rnfdmpr 41300 |
Copyright terms: Public domain | W3C validator |