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 4128 | . 2 ⊢ {𝐴, 𝐴} = ({𝐴} ∪ {𝐴}) | |
2 | unidm 3718 | . 2 ⊢ ({𝐴} ∪ {𝐴}) = {𝐴} | |
3 | 1, 2 | eqtr2i 2633 | 1 ⊢ {𝐴} = {𝐴, 𝐴} |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1475 ∪ cun 3538 {csn 4125 {cpr 4127 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 |
This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-clab 2597 df-cleq 2603 df-clel 2606 df-nfc 2740 df-v 3175 df-un 3545 df-pr 4128 |
This theorem is referenced by: nfsn 4189 disjprsn 4196 tpidm12 4234 tpidm 4237 preqsnd 4330 preqsn 4331 preqsnOLD 4332 elpreqprlem 4333 opid 4359 unisn 4387 intsng 4447 snex 4835 opeqsn 4892 propeqop 4895 relop 5194 funopg 5836 f1oprswap 6092 fnprb 6377 enpr1g 7908 supsn 8261 infsn 8293 prdom2 8712 wuntp 9412 wunsn 9417 grusn 9505 prunioo 12172 hashprg 13043 hashprgOLD 13044 hashfun 13084 lcmfsn 15186 lubsn 16917 indislem 20614 hmphindis 21410 wilthlem2 24595 upgrex 25759 umgrnloop0 25775 upgredg 25811 umgraex 25852 usgranloop0 25909 wlkntrllem1 26089 eupath2lem3 26506 1to2vfriswmgra 26533 esumpr2 29456 dvh2dim 35752 wopprc 36615 clsk1indlem4 37362 sge0prle 39294 meadjun 39355 opidg 40316 usgrnloop0ALT 40432 uspgr1v1eop 40475 1loopgruspgr 40715 1egrvtxdg0 40727 umgr2v2eedg 40740 umgr2v2e 40741 1wlkvtxeledglem 40827 ifpprsnss 40845 upgr1wlkwlk 40847 upgr11wlkdlem1 41312 1to2vfriswmgr 41449 |
Copyright terms: Public domain | W3C validator |