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 4564 | . 2 ⊢ {𝐴, 𝐴} = ({𝐴} ∪ {𝐴}) | |
2 | unidm 4086 | . 2 ⊢ ({𝐴} ∪ {𝐴}) = {𝐴} | |
3 | 1, 2 | eqtr2i 2767 | 1 ⊢ {𝐴} = {𝐴, 𝐴} |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1539 ∪ cun 3885 {csn 4561 {cpr 4563 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-ext 2709 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 845 df-tru 1542 df-ex 1783 df-sb 2068 df-clab 2716 df-cleq 2730 df-clel 2816 df-v 3434 df-un 3892 df-pr 4564 |
This theorem is referenced by: nfsn 4643 disjprsn 4650 tpidm12 4691 tpidm 4694 ifpprsnss 4700 preqsnd 4789 elpreqprlem 4796 opidg 4823 unisng 4860 intsng 4916 snex 5354 opeqsng 5417 propeqop 5421 relop 5759 funopg 6468 f1oprswap 6760 fnprb 7084 enpr1g 8810 supsn 9231 infsn 9264 prdom2 9762 wuntp 10467 wunsn 10472 grusn 10560 prunioo 13213 hashprg 14110 hashfun 14152 hashle2pr 14191 lcmfsn 16340 lubsn 18200 indislem 22150 hmphindis 22948 wilthlem2 26218 upgrex 27462 umgrnloop0 27479 edglnl 27513 usgrnloop0ALT 27572 uspgr1v1eop 27616 1loopgruspgr 27867 1egrvtxdg0 27878 umgr2v2eedg 27891 umgr2v2e 27892 ifpsnprss 27990 upgriswlk 28008 clwwlkn1 28405 upgr1wlkdlem1 28509 1to2vfriswmgr 28643 esumpr2 32035 dvh2dim 39459 wopprc 40852 clsk1indlem4 41654 sge0prle 43939 meadjun 44000 elsprel 44927 upgrwlkupwlk 45302 |
Copyright terms: Public domain | W3C validator |