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, see snprc 4647. For an alternate definition see dfsn2 4572. (Contributed by NM, 21-Jun-1993.) |
Ref | Expression |
---|---|
df-sn | ⊢ {𝐴} = {𝑥 ∣ 𝑥 = 𝐴} |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cA | . . 3 class 𝐴 | |
2 | 1 | csn 4559 | . 2 class {𝐴} |
3 | vx | . . . . 5 setvar 𝑥 | |
4 | 3 | cv 1527 | . . . 4 class 𝑥 |
5 | 4, 1 | wceq 1528 | . . 3 wff 𝑥 = 𝐴 |
6 | 5, 3 | cab 2799 | . 2 class {𝑥 ∣ 𝑥 = 𝐴} |
7 | 2, 6 | wceq 1528 | 1 wff {𝐴} = {𝑥 ∣ 𝑥 = 𝐴} |
Colors of variables: wff setvar class |
This definition is referenced by: sneq 4569 elsng 4573 absn 4577 dfsn2ALT 4579 rabsssn 4599 csbsng 4638 pw0 4739 iunid 4976 uniabio 6322 dfimafn2 6723 fnsnfv 6737 suppvalbr 7825 snec 8350 infmap2 9629 cf0 9662 cflecard 9664 brdom7disj 9942 brdom6disj 9943 vdwlem6 16312 hashbc0 16331 symgbas0 18453 psrbagsn 20205 ptcmplem2 22591 snclseqg 22653 nmoo0 28496 nmop0 29691 nmfn0 29692 disjabrex 30261 disjabrexf 30262 pstmfval 31036 hasheuni 31244 derang0 32314 dfiota3 33282 bj-nuliotaALT 34246 poimirlem28 34802 lineset 36756 frege54cor1c 40141 iotain 40629 csbsngVD 41107 dfaimafn2 43246 dfatsnafv2 43332 rnfdmpr 43361 efmndbas0 43958 |
Copyright terms: Public domain | W3C validator |