MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  dfsn2 Structured version   Visualization version   GIF version

Theorem dfsn2 4563
Description: Alternate definition of singleton. Definition 5.1 of [TakeutiZaring] p. 15. (Contributed by NM, 24-Apr-1994.)
Assertion
Ref Expression
dfsn2 {𝐴} = {𝐴, 𝐴}

Proof of Theorem dfsn2
StepHypRef Expression
1 df-pr 4553 . 2 {𝐴, 𝐴} = ({𝐴} ∪ {𝐴})
2 unidm 4114 . 2 ({𝐴} ∪ {𝐴}) = {𝐴}
31, 2eqtr2i 2848 1 {𝐴} = {𝐴, 𝐴}
Colors of variables: wff setvar class
Syntax hints:   = wceq 1538  cun 3917  {csn 4550  {cpr 4552
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-ext 2796
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-ex 1782  df-sb 2071  df-clab 2803  df-cleq 2817  df-clel 2896  df-v 3482  df-un 3924  df-pr 4553
This theorem is referenced by:  nfsn  4628  disjprsn  4635  tpidm12  4676  tpidm  4679  ifpprsnss  4685  preqsnd  4774  elpreqprlem  4781  opidg  4809  unisng  4844  intsng  4898  snex  5320  opeqsng  5381  propeqop  5385  relop  5709  funopg  6378  f1oprswap  6647  fnprb  6960  enpr1g  8567  supsn  8929  infsn  8962  prdom2  9426  wuntp  10127  wunsn  10132  grusn  10220  prunioo  12866  hashprg  13759  hashfun  13801  hashle2pr  13838  lcmfsn  15975  lubsn  17702  indislem  21603  hmphindis  22400  wilthlem2  25652  upgrex  26883  umgrnloop0  26900  edglnl  26934  usgrnloop0ALT  26993  uspgr1v1eop  27037  1loopgruspgr  27288  1egrvtxdg0  27299  umgr2v2eedg  27312  umgr2v2e  27313  ifpsnprss  27410  upgriswlk  27428  clwwlkn1  27824  upgr1wlkdlem1  27928  1to2vfriswmgr  28062  esumpr2  31353  dvh2dim  38653  wopprc  39827  clsk1indlem4  40606  sge0prle  42906  meadjun  42967  elsprel  43858  upgrwlkupwlk  44234
  Copyright terms: Public domain W3C validator