Theorem unisn 4930

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

Syntax hints:   = wceq 1541   ∈ wcel 2106  Vcvv 3474  {csn 4628  ∪ cuni 4908

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-v 3476  df-un 3953  df-in 3955  df-ss 3965  df-sn 4629  df-pr 4631  df-uni 4909

This theorem is referenced by:  unisnv  4931  unidif0  5358  op1sta  6224  op2nda  6227  opswap  6228  fvssunirnOLD  6925  funfv  6978  dffv2  6986  nlim1  8491  en1bOLD  9026  tc2  9739  cflim2  10260  fin1a2lem12  10408  acsmapd  18511  pmtrprfval  19396  lspuni0  20765  lss0v  20771  zrhval2  21277  indistopon  22724  refun0  23239  qtopeu  23440  hmphindis  23521  filconn  23607  ufildr  23655  cnextfres1  23792  bday1s  27557  old1  27595  madeoldsuc  27604  ghmquskerlem1  32790  dimval  32961  dimvalfi  32962  locfinref  33107  pstmfval  33162  esumval  33330  esumpfinval  33359  esumpfinvalf  33360  prsiga  33415  carsggect  33603  indispconn  34511  onsucsuccmpi  35631  bj-nuliotaALT  36242  heiborlem3  36984  isomenndlem  45545  uniimaelsetpreimafv  46363