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 4516 | . 2 ⊢ {𝐴, 𝐴} = ({𝐴} ∪ {𝐴}) | |
2 | unidm 4040 | . 2 ⊢ ({𝐴} ∪ {𝐴}) = {𝐴} | |
3 | 1, 2 | eqtr2i 2762 | 1 ⊢ {𝐴} = {𝐴, 𝐴} |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1542 ∪ cun 3839 {csn 4513 {cpr 4515 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1916 ax-6 1974 ax-7 2019 ax-8 2115 ax-9 2123 ax-ext 2710 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 847 df-tru 1545 df-ex 1787 df-sb 2074 df-clab 2717 df-cleq 2730 df-clel 2811 df-v 3399 df-un 3846 df-pr 4516 |
This theorem is referenced by: nfsn 4595 disjprsn 4602 tpidm12 4643 tpidm 4646 ifpprsnss 4652 preqsnd 4741 elpreqprlem 4748 opidg 4777 unisng 4814 intsng 4870 snex 5295 opeqsng 5357 propeqop 5361 relop 5687 funopg 6367 f1oprswap 6655 fnprb 6975 enpr1g 8615 supsn 9002 infsn 9035 prdom2 9499 wuntp 10204 wunsn 10209 grusn 10297 prunioo 12948 hashprg 13841 hashfun 13883 hashle2pr 13922 lcmfsn 16069 lubsn 17813 indislem 21744 hmphindis 22541 wilthlem2 25798 upgrex 27029 umgrnloop0 27046 edglnl 27080 usgrnloop0ALT 27139 uspgr1v1eop 27183 1loopgruspgr 27434 1egrvtxdg0 27445 umgr2v2eedg 27458 umgr2v2e 27459 ifpsnprss 27556 upgriswlk 27574 clwwlkn1 27970 upgr1wlkdlem1 28074 1to2vfriswmgr 28208 esumpr2 31597 dvh2dim 39071 wopprc 40408 clsk1indlem4 41184 sge0prle 43465 meadjun 43526 elsprel 44445 upgrwlkupwlk 44820 |
Copyright terms: Public domain | W3C validator |