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

Theorem dfsn2 3796
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 3789 . 2  |-  { A ,  A }  =  ( { A }  u.  { A } )
2 unidm 3458 . 2  |-  ( { A }  u.  { A } )  =  { A }
31, 2eqtr2i 2433 1  |-  { A }  =  { A ,  A }
Colors of variables: wff set class
Syntax hints:    = wceq 1649    u. cun 3286   {csn 3782   {cpr 3783
This theorem is referenced by:  nfsn  3834  tpidm12  3873  tpidm  3876  preqsn  3948  opid  3970  unisn  3999  intsng  4053  snex  4373  opeqsn  4420  relop  4990  funopg  5452  f1oprswap  5684  enpr1g  7140  supsn  7438  prdom2  7854  wuntp  8550  wunsn  8555  grusn  8643  prunioo  10989  hashprg  11629  hashfun  11663  lubsn  14486  indislem  17027  hmphindis  17790  wilthlem2  20813  umgraex  21319  usgranloop0  21361  wlkntrllem1  21520  eupath2lem3  21662  preqsnd  23961  esumpr2  24419  wopprc  26999  1to2vfriswmgra  28118  dvh2dim  31940
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2393
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2399  df-cleq 2405  df-clel 2408  df-nfc 2537  df-v 2926  df-un 3293  df-pr 3789
  Copyright terms: Public domain W3C validator