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

Theorem unisn 4823
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 unisn.1 . 2 𝐴 ∈ V
2 unisng 4822 . 2 (𝐴 ∈ V → {𝐴} = 𝐴)
31, 2ax-mp 5 1 {𝐴} = 𝐴
Colors of variables: wff setvar class
Syntax hints:   = wceq 1538  wcel 2112  Vcvv 3444  {csn 4528   cuni 4803
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-ext 2773
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-tru 1541  df-ex 1782  df-sb 2070  df-clab 2780  df-cleq 2794  df-clel 2873  df-v 3446  df-un 3889  df-in 3891  df-ss 3901  df-sn 4529  df-pr 4531  df-uni 4804
This theorem is referenced by:  uniintsn  4878  unidif0  5228  op1sta  6053  op2nda  6056  opswap  6057  unisuc  6239  uniabio  6301  fvssunirn  6678  opabiotafun  6723  funfv  6729  dffv2  6737  onuninsuci  7539  en1b  8564  tc2  9172  cflim2  9678  fin1a2lem10  9824  fin1a2lem12  9826  incexclem  15187  acsmapd  17784  pmtrprfval  18611  sylow2a  18740  lspuni0  19779  lss0v  19785  zrhval2  20206  indistopon  21610  refun0  22124  1stckgenlem  22162  qtopeu  22325  hmphindis  22406  filconn  22492  ufildr  22540  alexsubALTlem3  22658  ptcmplem2  22662  cnextfres1  22677  icccmplem1  23431  unidifsnel  30311  unidifsnne  30312  disjabrex  30349  disjabrexf  30350  dimval  31093  dimvalfi  31094  locfinref  31198  pstmfval  31253  esumval  31419  esumpfinval  31448  esumpfinvalf  31449  prsiga  31504  fiunelcarsg  31688  carsgclctunlem1  31689  carsggect  31690  indispconn  32595  fobigcup  33475  onsucsuccmpi  33905  bj-nuliotaALT  34476  mbfresfi  35102  heiborlem3  35250  isomenndlem  43162  uniimaelsetpreimafv  43906
  Copyright terms: Public domain W3C validator