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

Theorem unisn 3973
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 3771 . . 3  |-  { A }  =  { A ,  A }
21unieqi 3967 . 2  |-  U. { A }  =  U. { A ,  A }
3 unisn.1 . . 3  |-  A  e. 
_V
43, 3unipr 3971 . 2  |-  U. { A ,  A }  =  ( A  u.  A )
5 unidm 3433 . 2  |-  ( A  u.  A )  =  A
62, 4, 53eqtri 2411 1  |-  U. { A }  =  A
Colors of variables: wff set class
Syntax hints:    = wceq 1649    e. wcel 1717   _Vcvv 2899    u. cun 3261   {csn 3757   {cpr 3758   U.cuni 3957
This theorem is referenced by:  unisng  3974  uniintsn  4029  unidif0  4313  unisuc  4598  onuninsuci  4760  op1sta  5291  op2nda  5294  opswap  5296  uniabio  5368  fvssunirn  5694  funfv  5729  dffv2  5735  opabiotafun  6472  en1b  7111  tc2  7614  cflim2  8076  fin1a2lem10  8222  fin1a2lem12  8224  incexclem  12543  acsmapd  14531  sylow2a  15180  lspuni0  16013  lss0v  16019  zrhval2  16713  indistopon  16988  1stckgenlem  17506  qtopeu  17669  hmphindis  17750  filcon  17836  ufildr  17884  alexsubALTlem3  18001  ptcmplem2  18005  cnextfres  18020  icccmplem1  18724  disjabrex  23868  disjabrexf  23869  esumval  24237  esumpfinval  24261  esumpfinvalf  24262  prsiga  24310  indispcon  24700  fobigcup  25464  onsucsuccmpi  25907  heiborlem3  26213
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2368
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2374  df-cleq 2380  df-clel 2383  df-nfc 2512  df-rex 2655  df-v 2901  df-un 3268  df-sn 3763  df-pr 3764  df-uni 3958
  Copyright terms: Public domain W3C validator