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

Theorem unisn 3843
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 3654 . . 3  |-  { A }  =  { A ,  A }
21unieqi 3837 . 2  |-  U. { A }  =  U. { A ,  A }
3 unisn.1 . . 3  |-  A  e. 
_V
43, 3unipr 3841 . 2  |-  U. { A ,  A }  =  ( A  u.  A )
5 unidm 3318 . 2  |-  ( A  u.  A )  =  A
62, 4, 53eqtri 2307 1  |-  U. { A }  =  A
Colors of variables: wff set class
Syntax hints:    = wceq 1623    e. wcel 1684   _Vcvv 2788    u. cun 3150   {csn 3640   {cpr 3641   U.cuni 3827
This theorem is referenced by:  unisng  3844  uniintsn  3899  unidif0  4183  unisuc  4468  onuninsuci  4631  op1sta  5154  op2nda  5157  opswap  5159  uniabio  5229  fvssunirn  5551  funfv  5586  dffv2  5592  opabiotafun  6291  en1b  6929  tc2  7427  cflim2  7889  fin1a2lem10  8035  fin1a2lem12  8037  incexclem  12295  acsmapd  14281  sylow2a  14930  lspuni0  15767  lss0v  15773  zrhval2  16463  indistopon  16738  1stckgenlem  17248  qtopeu  17407  hmphindis  17488  filcon  17578  ufildr  17626  alexsubALTlem3  17743  ptcmplem2  17747  icccmplem1  18327  disjabrex  23359  disjabrexf  23360  esumval  23425  esumpfinval  23443  esumpfinvalf  23444  prsiga  23492  indispcon  23765  fobigcup  24440  onsucsuccmpi  24882  heiborlem3  26537
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-rex 2549  df-v 2790  df-un 3157  df-sn 3646  df-pr 3647  df-uni 3828
  Copyright terms: Public domain W3C validator