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

Theorem dfsn2 3878
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 3868 . 2  |-  { A ,  A }  =  ( { A }  u.  { A } )
2 unidm 3487 . 2  |-  ( { A }  u.  { A } )  =  { A }
31, 2eqtr2i 2454 1  |-  { A }  =  { A ,  A }
Colors of variables: wff setvar class
Syntax hints:    = wceq 1362    u. cun 3314   {csn 3865   {cpr 3867
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-v 2964  df-un 3321  df-pr 3868
This theorem is referenced by:  nfsn  3922  tpidm12  3964  tpidm  3967  preqsn  4043  opid  4066  unisn  4094  intsng  4151  snex  4521  opeqsn  4575  relop  4977  funopg  5438  f1oprswap  5668  fnprb  5923  enpr1g  7363  supsn  7707  prdom2  8161  wuntp  8865  wunsn  8870  grusn  8958  prunioo  11400  hashprg  12138  hashfun  12182  lubsn  15246  indislem  18445  hmphindis  19211  wilthlem2  22291  umgraex  23079  usgranloop0  23121  wlkntrllem1  23280  eupath2lem3  23422  preqsnd  25724  esumpr2  26370  wopprc  29221  1to2vfriswmgra  30441  dvh2dim  34660
  Copyright terms: Public domain W3C validator