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

Theorem dfsn2 4526
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 4516 . 2 {𝐴, 𝐴} = ({𝐴} ∪ {𝐴})
2 unidm 4040 . 2 ({𝐴} ∪ {𝐴}) = {𝐴}
31, 2eqtr2i 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