Theorem dfsn2 4584

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 4574	. 2 ⊢ {𝐴, 𝐴} = ({𝐴} ∪ {𝐴})
2		unidm 4102	. 2 ⊢ ({𝐴} ∪ {𝐴}) = {𝐴}
3	1, 2	eqtr2i 2755	1 ⊢ {𝐴} = {𝐴, 𝐴}

Syntax hints:   = wceq 1541   ∪ cun 3895  {csn 4571  {cpr 4573

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-v 3438  df-un 3902  df-pr 4574

This theorem is referenced by:  nfsn  4655  disjprsn  4662  tpidm12  4703  tpidm  4706  ifpprsnss  4712  preqsnd  4806  elpreqprlem  4813  opidg  4839  unisng  4872  intsng  4928  vsnex  5367  opeqsng  5438  propeqop  5442  relop  5785  funopg  6510  f1oprswap  6802  fnprb  7137  enpr1g  8940  prfi  9203  supsn  9352  infsn  9386  pr2ne  9891  prdom2  9892  wuntp  10597  wunsn  10602  grusn  10690  prunioo  13376  hashprg  14297  hashfun  14339  hashle2pr  14379  lcmfsn  16541  lubsn  18383  indislem  22910  hmphindis  23707  wilthlem2  27001  negs1s  27964  upgrex  29065  umgrnloop0  29082  edglnl  29116  usgrnloop0ALT  29178  uspgr1v1eop  29222  1loopgruspgr  29474  1egrvtxdg0  29485  umgr2v2eedg  29498  umgr2v2e  29499  ifpsnprss  29596  upgriswlk  29614  clwwlkn1  30013  upgr1wlkdlem1  30117  1to2vfriswmgr  30251  esumpr2  34072  dvh2dim  41484  wopprc  43063  clsk1indlem4  44077  sge0prle  46439  meadjun  46500  elsprel  47506  sclnbgrelself  47879  upgrwlkupwlk  48171