Theorem unisn 4861

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 4860	. 2 ⊢ (𝐴 ∈ V → ∪ {𝐴} = 𝐴)
3	1, 2	ax-mp 5	1 ⊢ ∪ {𝐴} = 𝐴

Syntax hints:   = wceq 1539   ∈ wcel 2106  Vcvv 3432  {csn 4561  ∪ cuni 4839

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-v 3434  df-un 3892  df-in 3894  df-ss 3904  df-sn 4562  df-pr 4564  df-uni 4840

This theorem is referenced by:  uniintsn  4918  unidif0  5282  op1sta  6128  op2nda  6131  opswap  6132  unisuc  6342  uniabio  6406  fvssunirn  6803  opabiotafun  6849  funfv  6855  dffv2  6863  onuninsuci  7687  nlim1  8319  en1b  8813  en1bOLD  8814  tc2  9500  cflim2  10019  fin1a2lem10  10165  fin1a2lem12  10167  incexclem  15548  acsmapd  18272  pmtrprfval  19095  sylow2a  19224  lspuni0  20272  lss0v  20278  zrhval2  20710  indistopon  22151  refun0  22666  1stckgenlem  22704  qtopeu  22867  hmphindis  22948  filconn  23034  ufildr  23082  alexsubALTlem3  23200  ptcmplem2  23204  cnextfres1  23219  icccmplem1  23985  unidifsnel  30883  unidifsnne  30884  disjabrex  30921  disjabrexf  30922  dimval  31686  dimvalfi  31687  locfinref  31791  pstmfval  31846  esumval  32014  esumpfinval  32043  esumpfinvalf  32044  prsiga  32099  fiunelcarsg  32283  carsgclctunlem1  32284  carsggect  32285  indispconn  33196  bday1s  34025  madeoldsuc  34067  fobigcup  34202  onsucsuccmpi  34632  bj-nuliotaALT  35229  mbfresfi  35823  heiborlem3  35971  sn-iotauni  40193  isomenndlem  44068  uniimaelsetpreimafv  44848