Theorem unisn 4882

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

Step	Hyp	Ref	Expression
1		unisn.1	. 2 ⊢ 𝐴 ∈ V
2		unisng 4881	. 2 ⊢ (𝐴 ∈ V → ∪ {𝐴} = 𝐴)
3	1, 2	ax-mp 5	1 ⊢ ∪ {𝐴} = 𝐴

Syntax hints:   = wceq 1541   ∈ wcel 2113  Vcvv 3440  {csn 4580  ∪ cuni 4863

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3442  df-un 3906  df-ss 3918  df-sn 4581  df-pr 4583  df-uni 4864

This theorem is referenced by:  unisnv  4883  unidif0  5305  op1sta  6183  op2nda  6186  opswap  6187  funfv  6921  dffv2  6929  nlim1  8416  tc2  9649  cflim2  10173  fin1a2lem12  10321  acsmapd  18477  ghmqusnsglem1  19209  ghmquskerlem1  19212  pmtrprfval  19416  lspuni0  20961  lss0v  20968  zrhval2  21463  indistopon  22945  refun0  23459  qtopeu  23660  hmphindis  23741  filconn  23827  ufildr  23875  cnextfres1  24012  bday1  27810  old1  27861  madeoldsuc  27881  dimval  33757  dimvalfi  33758  locfinref  33998  pstmfval  34053  esumval  34203  esumpfinval  34232  esumpfinvalf  34233  prsiga  34288  carsggect  34475  fineqvnttrclse  35280  indispconn  35428  onsucsuccmpi  36637  bj-nuliotaALT  37259  heiborlem3  38010  isomenndlem  46770  uniimaelsetpreimafv  47638