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

Theorem dfsn2 3830
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 3823 . 2  |-  { A ,  A }  =  ( { A }  u.  { A } )
2 unidm 3492 . 2  |-  ( { A }  u.  { A } )  =  { A }
31, 2eqtr2i 2459 1  |-  { A }  =  { A ,  A }
Colors of variables: wff set class
Syntax hints:    = wceq 1653    u. cun 3320   {csn 3816   {cpr 3817
This theorem is referenced by:  nfsn  3868  tpidm12  3907  tpidm  3910  preqsn  3982  opid  4004  unisn  4033  intsng  4087  snex  4407  opeqsn  4454  relop  5025  funopg  5487  f1oprswap  5719  enpr1g  7175  supsn  7476  prdom2  7892  wuntp  8588  wunsn  8593  grusn  8681  prunioo  11027  hashprg  11668  hashfun  11702  lubsn  14525  indislem  17066  hmphindis  17831  wilthlem2  20854  umgraex  21360  usgranloop0  21402  wlkntrllem1  21561  eupath2lem3  21703  preqsnd  24002  esumpr2  24460  wopprc  27103  1to2vfriswmgra  28398  dvh2dim  32245
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-v 2960  df-un 3327  df-pr 3823
  Copyright terms: Public domain W3C validator