| 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 4629 | . 2 ⊢ {𝐴, 𝐴} = ({𝐴} ∪ {𝐴}) | |
| 2 | unidm 4157 | . 2 ⊢ ({𝐴} ∪ {𝐴}) = {𝐴} | |
| 3 | 1, 2 | eqtr2i 2766 | 1 ⊢ {𝐴} = {𝐴, 𝐴} |
| Colors of variables: wff setvar class |
| Syntax hints: = wceq 1540 ∪ cun 3949 {csn 4626 {cpr 4628 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-tru 1543 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-v 3482 df-un 3956 df-pr 4629 |
| This theorem is referenced by: nfsn 4707 disjprsn 4714 tpidm12 4755 tpidm 4758 ifpprsnss 4764 preqsnd 4859 elpreqprlem 4866 opidg 4892 unisng 4925 intsng 4983 vsnex 5434 opeqsng 5508 propeqop 5512 relop 5861 funopg 6600 f1oprswap 6892 fnprb 7228 enpr1g 9063 prfi 9363 supsn 9512 infsn 9545 pr2ne 10044 prdom2 10046 wuntp 10751 wunsn 10756 grusn 10844 prunioo 13521 hashprg 14434 hashfun 14476 hashle2pr 14516 lcmfsn 16672 lubsn 18527 indislem 23007 hmphindis 23805 wilthlem2 27112 negs1s 28059 upgrex 29109 umgrnloop0 29126 edglnl 29160 usgrnloop0ALT 29222 uspgr1v1eop 29266 1loopgruspgr 29518 1egrvtxdg0 29529 umgr2v2eedg 29542 umgr2v2e 29543 ifpsnprss 29641 upgriswlk 29659 clwwlkn1 30060 upgr1wlkdlem1 30164 1to2vfriswmgr 30298 esumpr2 34068 dvh2dim 41447 wopprc 43042 clsk1indlem4 44057 sge0prle 46416 meadjun 46477 elsprel 47462 sclnbgrelself 47834 upgrwlkupwlk 48056 |
| Copyright terms: Public domain | W3C validator |