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

Theorem unisng 4265
Description: A set equals the union of its singleton. Theorem 8.2 of [Quine] p. 53. (Contributed by NM, 13-Aug-2002.)
Assertion
Ref Expression
unisng

Proof of Theorem unisng
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 sneq 4039 . . . 4
21unieqd 4259 . . 3
3 id 22 . . 3
42, 3eqeq12d 2479 . 2
5 vex 3112 . . 3
65unisn 4264 . 2
74, 6vtoclg 3167 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  =wceq 1395  e.wcel 1818  {csn 4029  U.cuni 4249
This theorem is referenced by:  unisn3  4266  dfnfc2  4267  unisn2  4588  en2other2  8408  pmtrprfv  16478  dprdsn  17083  indistopon  19502  ordtuni  19691  cmpcld  19902  ptcmplem5  20556  cldsubg  20609  icccmplem2  21328  vmappw  23390  chsupsn  26331  xrge0tsmseq  27777  esumsn  28072  prsiga  28131  cvmscld  28718  unisnif  29575  topjoin  30183  fnejoin2  30187  heiborlem8  30314  fourierdlem80  31969
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-rex 2813  df-v 3111  df-un 3480  df-sn 4030  df-pr 4032  df-uni 4250
  Copyright terms: Public domain W3C validator