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 4560 | . 2 ⊢ {𝐴, 𝐴} = ({𝐴} ∪ {𝐴}) | |
2 | unidm 4125 | . 2 ⊢ ({𝐴} ∪ {𝐴}) = {𝐴} | |
3 | 1, 2 | eqtr2i 2842 | 1 ⊢ {𝐴} = {𝐴, 𝐴} |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1528 ∪ cun 3931 {csn 4557 {cpr 4559 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-8 2107 ax-9 2115 ax-10 2136 ax-11 2151 ax-12 2167 ax-ext 2790 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 842 df-tru 1531 df-ex 1772 df-nf 1776 df-sb 2061 df-clab 2797 df-cleq 2811 df-clel 2890 df-nfc 2960 df-v 3494 df-un 3938 df-pr 4560 |
This theorem is referenced by: nfsn 4635 disjprsn 4642 tpidm12 4683 tpidm 4686 ifpprsnss 4692 preqsnd 4781 elpreqprlem 4788 opidg 4814 unisng 4845 intsng 4902 snex 5322 opeqsng 5384 propeqop 5388 relop 5714 funopg 6382 f1oprswap 6651 fnprb 6962 enpr1g 8563 supsn 8924 infsn 8957 prdom2 9420 wuntp 10121 wunsn 10126 grusn 10214 prunioo 12855 hashprg 13744 hashfun 13786 hashle2pr 13823 lcmfsn 15967 lubsn 17692 indislem 21536 hmphindis 22333 wilthlem2 25573 upgrex 26804 umgrnloop0 26821 edglnl 26855 usgrnloop0ALT 26914 uspgr1v1eop 26958 1loopgruspgr 27209 1egrvtxdg0 27220 umgr2v2eedg 27233 umgr2v2e 27234 ifpsnprss 27331 upgriswlk 27349 clwwlkn1 27746 upgr1wlkdlem1 27851 1to2vfriswmgr 27985 esumpr2 31225 dvh2dim 38461 wopprc 39505 clsk1indlem4 40272 sge0prle 42560 meadjun 42621 elsprel 43514 upgrwlkupwlk 43892 |
Copyright terms: Public domain | W3C validator |