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

Theorem unisn 4381
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 4137 . . 3 {𝐴} = {𝐴, 𝐴}
21unieqi 4375 . 2 {𝐴} = {𝐴, 𝐴}
3 unisn.1 . . 3 𝐴 ∈ V
43, 3unipr 4379 . 2 {𝐴, 𝐴} = (𝐴𝐴)
5 unidm 3717 . 2 (𝐴𝐴) = 𝐴
62, 4, 53eqtri 2635 1 {𝐴} = 𝐴
Colors of variables: wff setvar class
Syntax hints:   = wceq 1474  wcel 1976  Vcvv 3172  cun 3537  {csn 4124  {cpr 4126   cuni 4366
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-rex 2901  df-v 3174  df-un 3544  df-sn 4125  df-pr 4127  df-uni 4367
This theorem is referenced by:  unisng  4382  uniintsn  4443  unidif0  4758  op1sta  5520  op2nda  5523  opswap  5525  unisuc  5703  uniabio  5763  fvssunirn  6111  opabiotafun  6153  funfv  6159  dffv2  6165  onuninsuci  6909  en1b  7887  tc2  8478  cflim2  8945  fin1a2lem10  9091  fin1a2lem12  9093  incexclem  14355  acsmapd  16949  pmtrprfval  17678  sylow2a  17805  lspuni0  18779  lss0v  18785  zrhval2  19623  indistopon  20562  refun0  21075  1stckgenlem  21113  qtopeu  21276  hmphindis  21357  filcon  21444  ufildr  21492  alexsubALTlem3  21610  ptcmplem2  21614  cnextfres1  21629  icccmplem1  22380  disjabrex  28570  disjabrexf  28571  locfinref  29029  pstmfval  29060  esumval  29228  esumpfinval  29257  esumpfinvalf  29258  prsiga  29314  fiunelcarsg  29498  carsgclctunlem1  29499  carsggect  29500  indispcon  30263  fobigcup  30970  onsucsuccmpi  31405  bj-nuliotaALT  31994  mbfresfi  32409  heiborlem3  32565  prsal  38997  isomenndlem  39203
  Copyright terms: Public domain W3C validator