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

Theorem dfsn2 3655
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 3648 . 2  |-  { A ,  A }  =  ( { A }  u.  { A } )
2 unidm 3319 . 2  |-  ( { A }  u.  { A } )  =  { A }
31, 2eqtr2i 2305 1  |-  { A }  =  { A ,  A }
Colors of variables: wff set class
Syntax hints:    = wceq 1624    u. cun 3151   {csn 3641   {cpr 3642
This theorem is referenced by:  nfsn  3692  tpidm12  3729  tpidm  3732  preqsn  3793  opid  3815  unisn  3844  intsng  3898  snex  4215  opeqsn  4261  relop  4833  funopg  5252  f1oprswap  5480  enpr1g  6922  supsn  7215  prdom2  7631  wuntp  8328  wunsn  8333  grusn  8421  prunioo  10758  hashprg  11362  hashfun  11383  lubsn  14194  indislem  16731  hmphindis  17482  wilthlem2  20301  umgraex  23279  eupath2lem3  23307  singempcon  24992  wopprc  26522  dvh2dim  30902
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-gen 1534  ax-5 1545  ax-17 1604  ax-9 1637  ax-8 1645  ax-6 1704  ax-7 1709  ax-11 1716  ax-12 1867  ax-ext 2265
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1312  df-ex 1530  df-nf 1533  df-sb 1632  df-clab 2271  df-cleq 2277  df-clel 2280  df-nfc 2409  df-v 2791  df-un 3158  df-pr 3648
  Copyright terms: Public domain W3C validator