![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > dfsn2 | Structured version Visualization version GIF version |
Description: Alternate definition of singleton. Definition 5.1 of [TakeutiZaring] p. 15. (Contributed by NM, 24-Apr-1994.) |
Ref | Expression |
---|---|
dfsn2 | ⊢ {𝐴} = {𝐴, 𝐴} |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-pr 4623 | . 2 ⊢ {𝐴, 𝐴} = ({𝐴} ∪ {𝐴}) | |
2 | unidm 4144 | . 2 ⊢ ({𝐴} ∪ {𝐴}) = {𝐴} | |
3 | 1, 2 | eqtr2i 2753 | 1 ⊢ {𝐴} = {𝐴, 𝐴} |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1533 ∪ cun 3938 {csn 4620 {cpr 4622 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-ext 2695 |
This theorem depends on definitions: df-bi 206 df-an 396 df-or 845 df-tru 1536 df-ex 1774 df-sb 2060 df-clab 2702 df-cleq 2716 df-clel 2802 df-v 3468 df-un 3945 df-pr 4623 |
This theorem is referenced by: nfsn 4703 disjprsn 4710 tpidm12 4751 tpidm 4754 ifpprsnss 4760 preqsnd 4851 elpreqprlem 4858 opidg 4884 unisng 4919 intsng 4979 vsnex 5419 opeqsng 5493 propeqop 5497 relop 5840 funopg 6572 f1oprswap 6867 fnprb 7201 enpr1g 9015 supsn 9462 infsn 9495 pr2ne 9994 prdom2 9996 wuntp 10701 wunsn 10706 grusn 10794 prunioo 13454 hashprg 14351 hashfun 14393 hashle2pr 14434 lcmfsn 16568 lubsn 18434 indislem 22813 hmphindis 23611 wilthlem2 26905 upgrex 28776 umgrnloop0 28793 edglnl 28827 usgrnloop0ALT 28886 uspgr1v1eop 28930 1loopgruspgr 29181 1egrvtxdg0 29192 umgr2v2eedg 29205 umgr2v2e 29206 ifpsnprss 29304 upgriswlk 29322 clwwlkn1 29718 upgr1wlkdlem1 29822 1to2vfriswmgr 29956 esumpr2 33520 dvh2dim 40772 wopprc 42224 clsk1indlem4 43250 sge0prle 45568 meadjun 45629 elsprel 46594 upgrwlkupwlk 46969 |
Copyright terms: Public domain | W3C validator |