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

Theorem dfsn2 3991
Description: Alternate definition of singleton. Definition 5.1 of [TakeutiZaring] p. 15. (Contributed by NM, 24-Apr-1994.)
Assertion
Ref Expression
dfsn2  |-  { A }  =  { A ,  A }

Proof of Theorem dfsn2
StepHypRef Expression
1 df-pr 3981 . 2  |-  { A ,  A }  =  ( { A }  u.  { A } )
2 unidm 3600 . 2  |-  ( { A }  u.  { A } )  =  { A }
31, 2eqtr2i 2481 1  |-  { A }  =  { A ,  A }
Colors of variables: wff setvar class
Syntax hints:    = wceq 1370    u. cun 3427   {csn 3978   {cpr 3980
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2601  df-v 3073  df-un 3434  df-pr 3981
This theorem is referenced by:  nfsn  4035  tpidm12  4077  tpidm  4080  preqsn  4156  opid  4179  unisn  4207  intsng  4264  snex  4634  opeqsn  4688  relop  5091  funopg  5551  f1oprswap  5781  fnprb  6038  enpr1g  7478  supsn  7823  prdom2  8277  wuntp  8982  wunsn  8987  grusn  9075  prunioo  11524  hashprg  12266  hashfun  12310  lubsn  15375  indislem  18729  hmphindis  19495  wilthlem2  22533  umgraex  23402  usgranloop0  23444  wlkntrllem1  23603  eupath2lem3  23745  preqsnd  26046  esumpr2  26655  wopprc  29520  1to2vfriswmgra  30739  dvh2dim  35399
  Copyright terms: Public domain W3C validator