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

Theorem unisn 3845
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 3656 . . 3  |-  { A }  =  { A ,  A }
21unieqi 3839 . 2  |-  U. { A }  =  U. { A ,  A }
3 unisn.1 . . 3  |-  A  e. 
_V
43, 3unipr 3843 . 2  |-  U. { A ,  A }  =  ( A  u.  A )
5 unidm 3320 . 2  |-  ( A  u.  A )  =  A
62, 4, 53eqtri 2309 1  |-  U. { A }  =  A
Colors of variables: wff set class
Syntax hints:    = wceq 1625    e. wcel 1686   _Vcvv 2790    u. cun 3152   {csn 3642   {cpr 3643   U.cuni 3829
This theorem is referenced by:  unisng  3846  uniintsn  3901  unidif0  4185  unisuc  4470  onuninsuci  4633  op1sta  5156  op2nda  5159  opswap  5161  uniabio  5231  fvssunirn  5553  funfv  5588  dffv2  5594  opabiotafun  6293  en1b  6931  tc2  7429  cflim2  7891  fin1a2lem10  8037  fin1a2lem12  8039  incexclem  12297  acsmapd  14283  sylow2a  14932  lspuni0  15769  lss0v  15775  zrhval2  16465  indistopon  16740  1stckgenlem  17250  qtopeu  17409  hmphindis  17490  filcon  17580  ufildr  17628  alexsubALTlem3  17745  ptcmplem2  17749  icccmplem1  18329  disjabrex  23361  disjabrexf  23362  esumval  23427  esumpfinval  23445  esumpfinvalf  23446  prsiga  23494  indispcon  23767  fobigcup  24442  onsucsuccmpi  24884  heiborlem3  26548
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1535  ax-5 1546  ax-17 1605  ax-9 1637  ax-8 1645  ax-6 1705  ax-7 1710  ax-11 1717  ax-12 1868  ax-ext 2266
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1531  df-nf 1534  df-sb 1632  df-clab 2272  df-cleq 2278  df-clel 2281  df-nfc 2410  df-rex 2551  df-v 2792  df-un 3159  df-sn 3648  df-pr 3649  df-uni 3830
  Copyright terms: Public domain W3C validator