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

Theorem dfsn2 3558
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 3551 . 2  |-  { A ,  A }  =  ( { A }  u.  { A } )
2 unidm 3228 . 2  |-  ( { A }  u.  { A } )  =  { A }
31, 2eqtr2i 2274 1  |-  { A }  =  { A ,  A }
Colors of variables: wff set class
Syntax hints:    = wceq 1619    u. cun 3076   {csn 3544   {cpr 3545
This theorem is referenced by:  nfsn  3595  tpidm12  3632  tpidm  3635  preqsn  3692  opid  3714  unisn  3743  intsng  3795  snex  4110  opeqsn  4155  relop  4741  funopg  5144  f1oprswap  5372  enpr1g  6812  supsn  7104  prdom2  7520  wuntp  8213  wunsn  8218  grusn  8306  prunioo  10642  hashprg  11245  hashfun  11266  lubsn  14044  indislem  16569  hmphindis  17320  wilthlem2  20139  umgraex  23046  eupath2lem3  23074  singempcon  24759  wopprc  26289  dvh2dim  30324
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 1926  ax-ext 2234
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 1883  df-clab 2240  df-cleq 2246  df-clel 2249  df-nfc 2374  df-v 2729  df-un 3083  df-pr 3551
  Copyright terms: Public domain W3C validator