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

Theorem dfsn2 3614
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 3607 . 2  |-  { A ,  A }  =  ( { A }  u.  { A } )
2 unidm 3279 . 2  |-  ( { A }  u.  { A } )  =  { A }
31, 2eqtr2i 2277 1  |-  { A }  =  { A ,  A }
Colors of variables: wff set class
Syntax hints:    = wceq 1619    u. cun 3111   {csn 3600   {cpr 3601
This theorem is referenced by:  nfsn  3651  tpidm12  3688  tpidm  3691  preqsn  3752  opid  3774  unisn  3803  intsng  3857  snex  4174  opeqsn  4220  relop  4808  funopg  5211  f1oprswap  5439  enpr1g  6881  supsn  7174  prdom2  7590  wuntp  8287  wunsn  8292  grusn  8380  prunioo  10716  hashprg  11319  hashfun  11340  lubsn  14148  indislem  16685  hmphindis  17436  wilthlem2  20255  umgraex  23233  eupath2lem3  23261  singempcon  24946  wopprc  26476  dvh2dim  30786
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-11 1624  ax-17 1628  ax-12o 1664  ax-10 1678  ax-9 1684  ax-4 1692  ax-16 1927  ax-ext 2237
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1884  df-clab 2243  df-cleq 2249  df-clel 2252  df-nfc 2381  df-v 2759  df-un 3118  df-pr 3607
  Copyright terms: Public domain W3C validator