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

Theorem unisn 4846
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 4845 . 2 (𝐴 ∈ V → {𝐴} = 𝐴)
31, 2ax-mp 5 1 {𝐴} = 𝐴
Colors of variables: wff setvar class
Syntax hints:   = wceq 1528  wcel 2105  Vcvv 3492  {csn 4557   cuni 4830
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-rex 3141  df-v 3494  df-un 3938  df-sn 4558  df-pr 4560  df-uni 4831
This theorem is referenced by:  uniintsn  4904  unidif0  5251  op1sta  6075  op2nda  6078  opswap  6079  unisuc  6260  uniabio  6321  fvssunirn  6692  opabiotafun  6737  funfv  6743  dffv2  6749  onuninsuci  7544  en1b  8565  tc2  9172  cflim2  9673  fin1a2lem10  9819  fin1a2lem12  9821  incexclem  15179  acsmapd  17776  pmtrprfval  18544  sylow2a  18673  lspuni0  19711  lss0v  19717  zrhval2  20584  indistopon  21537  refun0  22051  1stckgenlem  22089  qtopeu  22252  hmphindis  22333  filconn  22419  ufildr  22467  alexsubALTlem3  22585  ptcmplem2  22589  cnextfres1  22604  icccmplem1  23357  unidifsnel  30222  unidifsnne  30223  disjabrex  30260  disjabrexf  30261  dimval  30900  dimvalfi  30901  locfinref  31004  pstmfval  31035  esumval  31204  esumpfinval  31233  esumpfinvalf  31234  prsiga  31289  fiunelcarsg  31473  carsgclctunlem1  31474  carsggect  31475  indispconn  32378  fobigcup  33258  onsucsuccmpi  33688  bj-nuliotaALT  34245  mbfresfi  34819  heiborlem3  34972  isomenndlem  42689  uniimaelsetpreimafv  43433
  Copyright terms: Public domain W3C validator