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

Theorem unisn 3784
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 3595 . . 3  |-  { A }  =  { A ,  A }
21unieqi 3778 . 2  |-  U. { A }  =  U. { A ,  A }
3 unisn.1 . . 3  |-  A  e. 
_V
43, 3unipr 3782 . 2  |-  U. { A ,  A }  =  ( A  u.  A )
5 unidm 3260 . 2  |-  ( A  u.  A )  =  A
62, 4, 53eqtri 2280 1  |-  U. { A }  =  A
Colors of variables: wff set class
Syntax hints:    = wceq 1619    e. wcel 1621   _Vcvv 2740    u. cun 3092   {csn 3581   {cpr 3582   U.cuni 3768
This theorem is referenced by:  unisng  3785  uniintsn  3840  unidif0  4121  unisuc  4405  onuninsuci  4568  op1sta  5106  op2nda  5109  opswap  5111  fvex  5437  fvssunirn  5450  funfv  5485  dffv2  5491  uniabio  6200  opabiotafun  6222  en1b  6862  tc2  7360  cflim2  7822  fin1a2lem10  7968  fin1a2lem12  7970  acsmapd  14208  sylow2a  14857  lspuni0  15694  lss0v  15700  zrhval2  16390  indistopon  16665  1stckgenlem  17175  qtopeu  17334  hmphindis  17415  filcon  17505  ufildr  17553  alexsubALTlem3  17670  ptcmplem2  17674  icccmplem1  18254  indispcon  23102  fobigcup  23781  onsucsuccmpi  24222  heiborlem3  25869
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 2237
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 2243  df-cleq 2249  df-clel 2252  df-nfc 2381  df-rex 2521  df-v 2742  df-un 3099  df-sn 3587  df-pr 3588  df-uni 3769
  Copyright terms: Public domain W3C validator