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

Theorem unisn 4023
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 3820 . . 3  |-  { A }  =  { A ,  A }
21unieqi 4017 . 2  |-  U. { A }  =  U. { A ,  A }
3 unisn.1 . . 3  |-  A  e. 
_V
43, 3unipr 4021 . 2  |-  U. { A ,  A }  =  ( A  u.  A )
5 unidm 3482 . 2  |-  ( A  u.  A )  =  A
62, 4, 53eqtri 2459 1  |-  U. { A }  =  A
Colors of variables: wff set class
Syntax hints:    = wceq 1652    e. wcel 1725   _Vcvv 2948    u. cun 3310   {csn 3806   {cpr 3807   U.cuni 4007
This theorem is referenced by:  unisng  4024  uniintsn  4079  unidif0  4364  unisuc  4649  onuninsuci  4812  op1sta  5343  op2nda  5346  opswap  5348  uniabio  5420  fvssunirn  5746  funfv  5782  dffv2  5788  opabiotafun  6528  en1b  7167  tc2  7673  cflim2  8135  fin1a2lem10  8281  fin1a2lem12  8283  incexclem  12608  acsmapd  14596  sylow2a  15245  lspuni0  16078  lss0v  16084  zrhval2  16782  indistopon  17057  1stckgenlem  17577  qtopeu  17740  hmphindis  17821  filcon  17907  ufildr  17955  alexsubALTlem3  18072  ptcmplem2  18076  cnextfres  18091  icccmplem1  18845  disjabrex  24016  disjabrexf  24017  pstmfval  24283  esumval  24433  esumpfinval  24457  esumpfinvalf  24458  prsiga  24506  indispcon  24913  fobigcup  25737  onsucsuccmpi  26185  mbfresfi  26243  heiborlem3  26513
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-rex 2703  df-v 2950  df-un 3317  df-sn 3812  df-pr 3813  df-uni 4008
  Copyright terms: Public domain W3C validator