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

Theorem unisn 3817
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 3628 . . 3  |-  { A }  =  { A ,  A }
21unieqi 3811 . 2  |-  U. { A }  =  U. { A ,  A }
3 unisn.1 . . 3  |-  A  e. 
_V
43, 3unipr 3815 . 2  |-  U. { A ,  A }  =  ( A  u.  A )
5 unidm 3293 . 2  |-  ( A  u.  A )  =  A
62, 4, 53eqtri 2282 1  |-  U. { A }  =  A
Colors of variables: wff set class
Syntax hints:    = wceq 1619    e. wcel 1621   _Vcvv 2763    u. cun 3125   {csn 3614   {cpr 3615   U.cuni 3801
This theorem is referenced by:  unisng  3818  uniintsn  3873  unidif0  4155  unisuc  4440  onuninsuci  4603  op1sta  5141  op2nda  5144  opswap  5146  fvex  5472  fvssunirn  5485  funfv  5520  dffv2  5526  uniabio  6235  opabiotafun  6257  en1b  6897  tc2  7395  cflim2  7857  fin1a2lem10  8003  fin1a2lem12  8005  acsmapd  14244  sylow2a  14893  lspuni0  15730  lss0v  15736  zrhval2  16426  indistopon  16701  1stckgenlem  17211  qtopeu  17370  hmphindis  17451  filcon  17541  ufildr  17589  alexsubALTlem3  17706  ptcmplem2  17710  icccmplem1  18290  indispcon  23138  fobigcup  23817  onsucsuccmpi  24258  heiborlem3  25905
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-11 1624  ax-17 1628  ax-12o 1664  ax-10 1678  ax-9 1684  ax-4 1692  ax-16 1927  ax-ext 2239
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1884  df-clab 2245  df-cleq 2251  df-clel 2254  df-nfc 2383  df-rex 2524  df-v 2765  df-un 3132  df-sn 3620  df-pr 3621  df-uni 3802
  Copyright terms: Public domain W3C validator