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

Theorem unisn 3844
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 3655 . . 3  |-  { A }  =  { A ,  A }
21unieqi 3838 . 2  |-  U. { A }  =  U. { A ,  A }
3 unisn.1 . . 3  |-  A  e. 
_V
43, 3unipr 3842 . 2  |-  U. { A ,  A }  =  ( A  u.  A )
5 unidm 3319 . 2  |-  ( A  u.  A )  =  A
62, 4, 53eqtri 2308 1  |-  U. { A }  =  A
Colors of variables: wff set class
Syntax hints:    = wceq 1623    e. wcel 1685   _Vcvv 2789    u. cun 3151   {csn 3641   {cpr 3642   U.cuni 3828
This theorem is referenced by:  unisng  3845  uniintsn  3900  unidif0  4182  unisuc  4467  onuninsuci  4630  op1sta  5152  op2nda  5155  opswap  5157  fvex  5500  fvssunirn  5513  funfv  5548  dffv2  5554  uniabio  6263  opabiotafun  6285  en1b  6925  tc2  7423  cflim2  7885  fin1a2lem10  8031  fin1a2lem12  8033  incexclem  12291  acsmapd  14277  sylow2a  14926  lspuni0  15763  lss0v  15769  zrhval2  16459  indistopon  16734  1stckgenlem  17244  qtopeu  17403  hmphindis  17484  filcon  17574  ufildr  17622  alexsubALTlem3  17739  ptcmplem2  17743  icccmplem1  18323  indispcon  23172  fobigcup  23851  onsucsuccmpi  24292  heiborlem3  25948
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 1636  ax-8 1644  ax-6 1704  ax-7 1709  ax-11 1716  ax-12 1868  ax-ext 2265
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 1631  df-clab 2271  df-cleq 2277  df-clel 2280  df-nfc 2409  df-rex 2550  df-v 2791  df-un 3158  df-sn 3647  df-pr 3648  df-uni 3829
  Copyright terms: Public domain W3C validator