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

Theorem unisn 3743
 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
Assertion
Ref Expression
unisn

Proof of Theorem unisn
StepHypRef Expression
1 dfsn2 3558 . . 3
21unieqi 3737 . 2
3 unisn.1 . . 3
43, 3unipr 3741 . 2
5 unidm 3228 . 2
62, 4, 53eqtri 2277 1
 Colors of variables: wff set class Syntax hints:   wceq 1619   wcel 1621  cvv 2727   cun 3076  csn 3544  cpr 3545  cuni 3727 This theorem is referenced by:  unisng  3744  uniintsn  3797  unidif0  4077  unisuc  4361  onuninsuci  4522  op1sta  5060  op2nda  5063  opswap  5065  fvex  5391  fvssunirn  5404  funfv  5438  dffv2  5444  uniabio  6153  opabiotafun  6175  en1b  6814  tc2  7311  cflim2  7773  fin1a2lem10  7919  fin1a2lem12  7921  sylow2a  14765  lspuni0  15602  lss0v  15608  zrhval2  16295  indistopon  16570  1stckgenlem  17080  qtopeu  17239  hmphindis  17320  filcon  17410  ufildr  17458  alexsubALTlem3  17575  ptcmplem2  17579  icccmplem1  18159  indispcon  22936  fobigcup  23615  onsucsuccmpi  24056  heiborlem3  25703 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 1926  ax-ext 2234 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 1883  df-clab 2240  df-cleq 2246  df-clel 2249  df-nfc 2374  df-rex 2514  df-v 2729  df-un 3083  df-sn 3550  df-pr 3551  df-uni 3728
 Copyright terms: Public domain W3C validator