Theorem unisn 4881

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

Syntax hints:   = wceq 1559   ∈ wcel 2141  Vcvv 3453  {csn 4579  ∪ cuni 4862

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-tru 1562  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3455  df-un 3907  df-ss 3919  df-sn 4580  df-pr 4582  df-uni 4863

This theorem is referenced by:  unisnv  4882  unidif0  5313  unidif0OLD  5314  op1sta  6207  op2nda  6210  opswap  6211  funfv  6949  dffv2  6957  nlim1  8452  tc2  9689  cflim2  10214  fin1a2lem12  10362  acsmapd  18577  ghmqusnsglem1  19311  ghmquskerlem1  19314  pmtrprfval  19518  lspuni0  21065  lss0v  21071  zrhval2  21548  indistopon  23049  refun0  23563  qtopeu  23764  hmphindis  23845  filconn  23931  ufildr  23979  cnextfres1  24116  bday1  27895  old1  27946  madeoldsuc  27966  dimval  33859  dimvalfi  33860  locfinref  34099  pstmfval  34154  esumval  34304  esumpfinval  34333  esumpfinvalf  34334  prsiga  34389  carsggect  34576  fineqvnttrclse  35381  indispconn  35545  onsucsuccmpi  36764  bj-nuliotaALT  37504  heiborlem3  38273  isomenndlem  47065  uniimaelsetpreimafv  47963