![]() |
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 4401 | . 2 ⊢ {𝐴, 𝐴} = ({𝐴} ∪ {𝐴}) | |
2 | unidm 3979 | . 2 ⊢ ({𝐴} ∪ {𝐴}) = {𝐴} | |
3 | 1, 2 | eqtr2i 2803 | 1 ⊢ {𝐴} = {𝐴, 𝐴} |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1601 ∪ cun 3790 {csn 4398 {cpr 4400 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1839 ax-4 1853 ax-5 1953 ax-6 2021 ax-7 2055 ax-9 2116 ax-10 2135 ax-11 2150 ax-12 2163 ax-ext 2754 |
This theorem depends on definitions: df-bi 199 df-an 387 df-or 837 df-tru 1605 df-ex 1824 df-nf 1828 df-sb 2012 df-clab 2764 df-cleq 2770 df-clel 2774 df-nfc 2921 df-v 3400 df-un 3797 df-pr 4401 |
This theorem is referenced by: nfsn 4474 disjprsn 4481 tpidm12 4522 tpidm 4525 ifpprsnss 4531 preqsnd 4620 preqsndOLD 4621 preqsnOLD 4625 elpreqprlem 4629 opidg 4655 unisng 4686 unisnOLD 4688 intsng 4745 snex 5140 opeqsng 5198 opeqsnOLD 5200 propeqop 5204 relop 5518 funopg 6169 f1oprswap 6434 fnprb 6744 enpr1g 8307 supsn 8666 infsn 8699 prdom2 9162 wuntp 9868 wunsn 9873 grusn 9961 prunioo 12618 hashprg 13497 hashfun 13538 hashle2pr 13573 lcmfsn 15754 lubsn 17480 indislem 21212 hmphindis 22009 wilthlem2 25247 upgrex 26440 umgrnloop0 26457 edglnl 26492 usgrnloop0ALT 26551 uspgr1v1eop 26596 1loopgruspgr 26848 1egrvtxdg0 26859 umgr2v2eedg 26872 umgr2v2e 26873 ifpsnprss 26970 upgriswlk 26988 clwwlkn1 27431 upgr1wlkdlem1 27548 1to2vfriswmgr 27687 esumpr2 30727 dvh2dim 37601 wopprc 38560 clsk1indlem4 39302 sge0prle 41546 meadjun 41607 elsprel 42418 upgrwlkupwlk 42767 |
Copyright terms: Public domain | W3C validator |