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

Theorem dfsn2 4137
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 4127 . 2 {𝐴, 𝐴} = ({𝐴} ∪ {𝐴})
2 unidm 3717 . 2 ({𝐴} ∪ {𝐴}) = {𝐴}
31, 2eqtr2i 2632 1 {𝐴} = {𝐴, 𝐴}
Colors of variables: wff setvar class
Syntax hints:   = wceq 1474  cun 3537  {csn 4124  {cpr 4126
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-v 3174  df-un 3544  df-pr 4127
This theorem is referenced by:  nfsn  4188  disjprsn  4195  tpidm12  4233  tpidm  4236  preqsnd  4325  preqsn  4326  preqsnOLD  4327  elpreqprlem  4328  opid  4353  unisn  4381  intsng  4441  snex  4830  opeqsn  4886  relop  5182  funopg  5822  f1oprswap  6077  fnprb  6355  enpr1g  7886  supsn  8239  infsn  8271  prdom2  8690  wuntp  9390  wunsn  9395  grusn  9483  prunioo  12131  hashprg  12998  hashprgOLD  12999  hashfun  13039  lcmfsn  15135  lubsn  16866  indislem  20562  hmphindis  21358  wilthlem2  24540  umgraex  25646  usgranloop0  25703  wlkntrllem1  25883  eupath2lem3  26300  1to2vfriswmgra  26327  esumpr2  29290  dvh2dim  35576  wopprc  36439  clsk1indlem4  37186  sge0prle  39118  meadjun  39179  opidg  40144  propeqop  40146  upgrex  40340  umgrnloop0  40356  upgredg  40392  usgrnloop0ALT  40454  uspgr1v1eop  40497  1loopgruspgr  40737  1egrvtxdg0  40749  umgr2v2eedg  40762  umgr2v2e  40763  1wlkvtxeledglem  40849  ifpprsnss  40867  upgr1wlkwlk  40869  upgr11wlkdlem1  41334  1to2vfriswmgr  41471
  Copyright terms: Public domain W3C validator