Theorem dfsn2 4538

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

Step	Hyp	Ref	Expression
1		df-pr 4528	. 2 ⊢ {𝐴, 𝐴} = ({𝐴} ∪ {𝐴})
2		unidm 4079	. 2 ⊢ ({𝐴} ∪ {𝐴}) = {𝐴}
3	1, 2	eqtr2i 2822	1 ⊢ {𝐴} = {𝐴, 𝐴}

Syntax hints:   = wceq 1538   ∪ cun 3879  {csn 4525  {cpr 4527

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-un 3886  df-pr 4528

This theorem is referenced by:  nfsn  4603  disjprsn  4610  tpidm12  4651  tpidm  4654  ifpprsnss  4660  preqsnd  4749  elpreqprlem  4756  opidg  4784  unisng  4819  intsng  4873  snex  5297  opeqsng  5358  propeqop  5362  relop  5685  funopg  6358  f1oprswap  6633  fnprb  6948  enpr1g  8558  supsn  8920  infsn  8953  prdom2  9417  wuntp  10122  wunsn  10127  grusn  10215  prunioo  12859  hashprg  13752  hashfun  13794  hashle2pr  13831  lcmfsn  15969  lubsn  17696  indislem  21605  hmphindis  22402  wilthlem2  25654  upgrex  26885  umgrnloop0  26902  edglnl  26936  usgrnloop0ALT  26995  uspgr1v1eop  27039  1loopgruspgr  27290  1egrvtxdg0  27301  umgr2v2eedg  27314  umgr2v2e  27315  ifpsnprss  27412  upgriswlk  27430  clwwlkn1  27826  upgr1wlkdlem1  27930  1to2vfriswmgr  28064  esumpr2  31436  dvh2dim  38741  wopprc  39971  clsk1indlem4  40747  sge0prle  43040  meadjun  43101  elsprel  43992  upgrwlkupwlk  44368