Theorem dfsn2 4574

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 4564	. 2 ⊢ {𝐴, 𝐴} = ({𝐴} ∪ {𝐴})
2		unidm 4086	. 2 ⊢ ({𝐴} ∪ {𝐴}) = {𝐴}
3	1, 2	eqtr2i 2767	1 ⊢ {𝐴} = {𝐴, 𝐴}

Syntax hints:   = wceq 1539   ∪ cun 3885  {csn 4561  {cpr 4563

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-v 3434  df-un 3892  df-pr 4564

This theorem is referenced by:  nfsn  4643  disjprsn  4650  tpidm12  4691  tpidm  4694  ifpprsnss  4700  preqsnd  4789  elpreqprlem  4796  opidg  4823  unisng  4860  intsng  4916  snex  5354  opeqsng  5417  propeqop  5421  relop  5759  funopg  6468  f1oprswap  6760  fnprb  7084  enpr1g  8810  supsn  9231  infsn  9264  prdom2  9762  wuntp  10467  wunsn  10472  grusn  10560  prunioo  13213  hashprg  14110  hashfun  14152  hashle2pr  14191  lcmfsn  16340  lubsn  18200  indislem  22150  hmphindis  22948  wilthlem2  26218  upgrex  27462  umgrnloop0  27479  edglnl  27513  usgrnloop0ALT  27572  uspgr1v1eop  27616  1loopgruspgr  27867  1egrvtxdg0  27878  umgr2v2eedg  27891  umgr2v2e  27892  ifpsnprss  27990  upgriswlk  28008  clwwlkn1  28405  upgr1wlkdlem1  28509  1to2vfriswmgr  28643  esumpr2  32035  dvh2dim  39459  wopprc  40852  clsk1indlem4  41654  sge0prle  43939  meadjun  44000  elsprel  44927  upgrwlkupwlk  45302