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

Theorem unisn 4387
 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 𝐴 ∈ V
Assertion
Ref Expression
unisn {𝐴} = 𝐴

Proof of Theorem unisn
StepHypRef Expression
1 dfsn2 4138 . . 3 {𝐴} = {𝐴, 𝐴}
21unieqi 4381 . 2 {𝐴} = {𝐴, 𝐴}
3 unisn.1 . . 3 𝐴 ∈ V
43, 3unipr 4385 . 2 {𝐴, 𝐴} = (𝐴𝐴)
5 unidm 3718 . 2 (𝐴𝐴) = 𝐴
62, 4, 53eqtri 2636 1 {𝐴} = 𝐴
 Colors of variables: wff setvar class Syntax hints:   = wceq 1475   ∈ wcel 1977  Vcvv 3173   ∪ cun 3538  {csn 4125  {cpr 4127  ∪ cuni 4372 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-rex 2902  df-v 3175  df-un 3545  df-sn 4126  df-pr 4128  df-uni 4373 This theorem is referenced by:  unisng  4388  uniintsn  4449  unidif0  4764  op1sta  5535  op2nda  5538  opswap  5540  unisuc  5718  uniabio  5778  fvssunirn  6127  opabiotafun  6169  funfv  6175  dffv2  6181  onuninsuci  6932  en1b  7910  tc2  8501  cflim2  8968  fin1a2lem10  9114  fin1a2lem12  9116  incexclem  14407  acsmapd  17001  pmtrprfval  17730  sylow2a  17857  lspuni0  18831  lss0v  18837  zrhval2  19676  indistopon  20615  refun0  21128  1stckgenlem  21166  qtopeu  21329  hmphindis  21410  filcon  21497  ufildr  21545  alexsubALTlem3  21663  ptcmplem2  21667  cnextfres1  21682  icccmplem1  22433  disjabrex  28777  disjabrexf  28778  locfinref  29236  pstmfval  29267  esumval  29435  esumpfinval  29464  esumpfinvalf  29465  prsiga  29521  fiunelcarsg  29705  carsgclctunlem1  29706  carsggect  29707  indispcon  30470  fobigcup  31177  onsucsuccmpi  31612  bj-nuliotaALT  32211  mbfresfi  32626  heiborlem3  32782  prsal  39214  isomenndlem  39420
 Copyright terms: Public domain W3C validator