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

Theorem unisn 4106
Description: A set equals the union of its singleton. Theorem 8.2 of [Quine] p. 53. (Contributed by NM, 30-Aug-1993.)
Hypothesis
Ref Expression
unisn.1  |-  A  e. 
_V
Assertion
Ref Expression
unisn  |-  U. { A }  =  A

Proof of Theorem unisn
StepHypRef Expression
1 dfsn2 3890 . . 3  |-  { A }  =  { A ,  A }
21unieqi 4100 . 2  |-  U. { A }  =  U. { A ,  A }
3 unisn.1 . . 3  |-  A  e. 
_V
43, 3unipr 4104 . 2  |-  U. { A ,  A }  =  ( A  u.  A )
5 unidm 3499 . 2  |-  ( A  u.  A )  =  A
62, 4, 53eqtri 2467 1  |-  U. { A }  =  A
Colors of variables: wff setvar class
Syntax hints:    = wceq 1369    e. wcel 1756   _Vcvv 2972    u. cun 3326   {csn 3877   {cpr 3879   U.cuni 4091
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2568  df-rex 2721  df-v 2974  df-un 3333  df-sn 3878  df-pr 3880  df-uni 4092
This theorem is referenced by:  unisng  4107  uniintsn  4165  unidif0  4465  unisuc  4795  op1sta  5321  op2nda  5324  opswap  5326  uniabio  5391  fvssunirn  5713  opabiotafun  5752  funfv  5758  dffv2  5764  onuninsuci  6451  en1b  7377  tc2  7962  cflim2  8432  fin1a2lem10  8578  fin1a2lem12  8580  incexclem  13299  acsmapd  15348  pmtrprfval  15993  sylow2a  16118  lspuni0  17091  lss0v  17097  zrhval2  17940  indistopon  18605  1stckgenlem  19126  qtopeu  19289  hmphindis  19370  filcon  19456  ufildr  19504  alexsubALTlem3  19621  ptcmplem2  19625  cnextfres  19640  icccmplem1  20399  disjabrex  25926  disjabrexf  25927  pstmfval  26323  esumval  26500  esumpfinval  26524  esumpfinvalf  26525  prsiga  26574  indispcon  27123  fobigcup  27931  onsucsuccmpi  28289  mbfresfi  28438  heiborlem3  28712
  Copyright terms: Public domain W3C validator