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 4653. For an alternate definition see dfsn2 4574. (Contributed by NM, 21-Jun-1993.) |
Ref | Expression |
---|---|
df-sn | ⊢ {𝐴} = {𝑥 ∣ 𝑥 = 𝐴} |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cA | . . 3 class 𝐴 | |
2 | 1 | csn 4561 | . 2 class {𝐴} |
3 | vx | . . . . 5 setvar 𝑥 | |
4 | 3 | cv 1538 | . . . 4 class 𝑥 |
5 | 4, 1 | wceq 1539 | . . 3 wff 𝑥 = 𝐴 |
6 | 5, 3 | cab 2715 | . 2 class {𝑥 ∣ 𝑥 = 𝐴} |
7 | 2, 6 | wceq 1539 | 1 wff {𝐴} = {𝑥 ∣ 𝑥 = 𝐴} |
Colors of variables: wff setvar class |
This definition is referenced by: sneq 4571 elsng 4575 absn 4579 dfsn2ALT 4581 rabsssn 4603 csbsng 4644 pw0 4745 iunid 4990 uniabio 6406 dfimafn2 6833 fnsnfvOLD 6848 suppvalbr 7981 snec 8569 fset0 8642 0map0sn0 8673 infmap2 9974 cf0 10007 cflecard 10009 brdom7disj 10287 brdom6disj 10288 vdwlem6 16687 hashbc0 16706 symgbas0 18996 psrbagsn 21271 ptcmplem2 23204 snclseqg 23267 nmoo0 29153 nmop0 30348 nmfn0 30349 disjabrex 30921 disjabrexf 30922 pstmfval 31846 hasheuni 32053 derang0 33131 dfiota3 34225 bj-nuliotaALT 35229 poimirlem28 35805 lineset 37752 abbi1sn 40191 frege54cor1c 41523 iotain 42035 csbsngVD 42513 dfaimafn2 44658 dfatsnafv2 44744 rnfdmpr 44773 |
Copyright terms: Public domain | W3C validator |