Theorem dfsn2 4595

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 4585	. 2 ⊢ {𝐴, 𝐴} = ({𝐴} ∪ {𝐴})
2		unidm 4111	. 2 ⊢ ({𝐴} ∪ {𝐴}) = {𝐴}
3	1, 2	eqtr2i 2761	1 ⊢ {𝐴} = {𝐴, 𝐴}

Syntax hints:   = wceq 1542   ∪ cun 3901  {csn 4582  {cpr 4584

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3444  df-un 3908  df-pr 4585

This theorem is referenced by:  nfsn  4666  disjprsn  4673  tpidm12  4714  tpidm  4717  ifpprsnss  4723  preqsnd  4817  elpreqprlem  4824  opidg  4850  unisng  4883  intsng  4940  vsnex  5381  snex  5385  opeqsng  5459  propeqop  5463  relop  5807  funopg  6534  f1oprswap  6827  fnprb  7164  enpr1g  8972  prfi  9236  supsn  9388  infsn  9422  pr2ne  9927  prdom2  9928  wuntp  10634  wunsn  10639  grusn  10727  prunioo  13409  hashprg  14330  hashfun  14372  hashle2pr  14412  lcmfsn  16574  lubsn  18417  indislem  22956  hmphindis  23753  wilthlem2  27047  neg1s  28035  upgrex  29177  umgrnloop0  29194  edglnl  29228  usgrnloop0ALT  29290  uspgr1v1eop  29334  1loopgruspgr  29586  1egrvtxdg0  29597  umgr2v2eedg  29610  umgr2v2e  29611  ifpsnprss  29708  upgriswlk  29726  clwwlkn1  30128  upgr1wlkdlem1  30232  1to2vfriswmgr  30366  esumpr2  34245  dvh2dim  41821  wopprc  43387  clsk1indlem4  44400  sge0prle  46759  meadjun  46820  elsprel  47835  sclnbgrelself  48208  upgrwlkupwlk  48500