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

Theorem unisn 3859
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 3667 . . 3  |-  { A }  =  { A ,  A }
21unieqi 3853 . 2  |-  U. { A }  =  U. { A ,  A }
3 unisn.1 . . 3  |-  A  e. 
_V
43, 3unipr 3857 . 2  |-  U. { A ,  A }  =  ( A  u.  A )
5 unidm 3331 . 2  |-  ( A  u.  A )  =  A
62, 4, 53eqtri 2320 1  |-  U. { A }  =  A
Colors of variables: wff set class
Syntax hints:    = wceq 1632    e. wcel 1696   _Vcvv 2801    u. cun 3163   {csn 3653   {cpr 3654   U.cuni 3843
This theorem is referenced by:  unisng  3860  uniintsn  3915  unidif0  4199  unisuc  4484  onuninsuci  4647  op1sta  5170  op2nda  5173  opswap  5175  uniabio  5245  fvssunirn  5567  funfv  5602  dffv2  5608  opabiotafun  6307  en1b  6945  tc2  7443  cflim2  7905  fin1a2lem10  8051  fin1a2lem12  8053  incexclem  12311  acsmapd  14297  sylow2a  14946  lspuni0  15783  lss0v  15789  zrhval2  16479  indistopon  16754  1stckgenlem  17264  qtopeu  17423  hmphindis  17504  filcon  17594  ufildr  17642  alexsubALTlem3  17759  ptcmplem2  17763  icccmplem1  18343  disjabrex  23374  disjabrexf  23375  esumval  23440  esumpfinval  23458  esumpfinvalf  23459  prsiga  23507  indispcon  23780  fobigcup  24511  onsucsuccmpi  24954  heiborlem3  26640
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-rex 2562  df-v 2803  df-un 3170  df-sn 3659  df-pr 3660  df-uni 3844
  Copyright terms: Public domain W3C validator