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

Theorem unisng 4602
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 4329 . . . 4 (𝑥 = 𝐴 → {𝑥} = {𝐴})
21unieqd 4596 . . 3 (𝑥 = 𝐴 {𝑥} = {𝐴})
3 id 22 . . 3 (𝑥 = 𝐴𝑥 = 𝐴)
42, 3eqeq12d 2773 . 2 (𝑥 = 𝐴 → ( {𝑥} = 𝑥 {𝐴} = 𝐴))
5 vex 3341 . . 3 𝑥 ∈ V
65unisn 4601 . 2 {𝑥} = 𝑥
74, 6vtoclg 3404 1 (𝐴𝑉 {𝐴} = 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1630  wcel 2137  {csn 4319   cuni 4586
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1869  ax-4 1884  ax-5 1986  ax-6 2052  ax-7 2088  ax-9 2146  ax-10 2166  ax-11 2181  ax-12 2194  ax-13 2389  ax-ext 2738
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1633  df-ex 1852  df-nf 1857  df-sb 2045  df-clab 2745  df-cleq 2751  df-clel 2754  df-nfc 2889  df-rex 3054  df-v 3340  df-un 3718  df-sn 4320  df-pr 4322  df-uni 4587
This theorem is referenced by:  unisn3  4603  dfnfc2  4604  dfnfc2OLD  4605  unisn2  4944  en2other2  9020  pmtrprfv  18071  dprdsn  18633  indistopon  21005  ordtuni  21194  cmpcld  21405  ptcmplem5  22059  cldsubg  22113  icccmplem2  22825  vmappw  25039  chsupsn  28579  xrge0tsmseq  30094  esumsnf  30433  prsiga  30501  rossros  30550  cvmscld  31560  unisnif  32336  topjoin  32664  fnejoin2  32668  bj-snmoore  33372  heiborlem8  33928  fourierdlem80  40904
  Copyright terms: Public domain W3C validator