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

Theorem unisn 3995
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 3792 . . 3  |-  { A }  =  { A ,  A }
21unieqi 3989 . 2  |-  U. { A }  =  U. { A ,  A }
3 unisn.1 . . 3  |-  A  e. 
_V
43, 3unipr 3993 . 2  |-  U. { A ,  A }  =  ( A  u.  A )
5 unidm 3454 . 2  |-  ( A  u.  A )  =  A
62, 4, 53eqtri 2432 1  |-  U. { A }  =  A
Colors of variables: wff set class
Syntax hints:    = wceq 1649    e. wcel 1721   _Vcvv 2920    u. cun 3282   {csn 3778   {cpr 3779   U.cuni 3979
This theorem is referenced by:  unisng  3996  uniintsn  4051  unidif0  4336  unisuc  4621  onuninsuci  4783  op1sta  5314  op2nda  5317  opswap  5319  uniabio  5391  fvssunirn  5717  funfv  5753  dffv2  5759  opabiotafun  6499  en1b  7138  tc2  7641  cflim2  8103  fin1a2lem10  8249  fin1a2lem12  8251  incexclem  12575  acsmapd  14563  sylow2a  15212  lspuni0  16045  lss0v  16051  zrhval2  16749  indistopon  17024  1stckgenlem  17542  qtopeu  17705  hmphindis  17786  filcon  17872  ufildr  17920  alexsubALTlem3  18037  ptcmplem2  18041  cnextfres  18056  icccmplem1  18810  disjabrex  23981  disjabrexf  23982  pstmfval  24248  esumval  24398  esumpfinval  24422  esumpfinvalf  24423  prsiga  24471  indispcon  24878  fobigcup  25658  onsucsuccmpi  26101  mbfresfi  26156  heiborlem3  26416
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2389
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2395  df-cleq 2401  df-clel 2404  df-nfc 2533  df-rex 2676  df-v 2922  df-un 3289  df-sn 3784  df-pr 3785  df-uni 3980
  Copyright terms: Public domain W3C validator