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

Theorem dfsn2 4011
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 4001 . 2  |-  { A ,  A }  =  ( { A }  u.  { A } )
2 unidm 3609 . 2  |-  ( { A }  u.  { A } )  =  { A }
31, 2eqtr2i 2452 1  |-  { A }  =  { A ,  A }
Colors of variables: wff setvar class
Syntax hints:    = wceq 1437    u. cun 3434   {csn 3998   {cpr 4000
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2057  ax-ext 2401
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2568  df-v 3082  df-un 3441  df-pr 4001
This theorem is referenced by:  nfsn  4057  tpidm12  4101  tpidm  4104  preqsn  4183  opid  4206  unisn  4234  intsng  4291  snex  4662  opeqsn  4716  relop  5004  funopg  5633  f1oprswap  5870  fnprb  6138  enpr1g  7645  supsn  7997  infsn  8029  prdom2  8445  wuntp  9143  wunsn  9148  grusn  9236  prunioo  11768  hashprg  12578  hashfun  12613  lcmfsn  14607  lubsn  16339  indislem  20013  hmphindis  20810  wilthlem2  23992  umgraex  25048  usgranloop0  25105  wlkntrllem1  25287  eupath2lem3  25705  1to2vfriswmgra  25732  preqsnd  28159  esumpr2  28896  dvh2dim  34982  wopprc  35855  sge0prle  38151  meadjun  38208  opidg  38863  propeqop  38865  umgrex  39011  usgrnloop0  39071  umgredg  39077
  Copyright terms: Public domain W3C validator