Theorem unisn 4880

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

Syntax hints:   = wceq 1540   ∈ wcel 2109  Vcvv 3438  {csn 4579  ∪ cuni 4861

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3440  df-un 3910  df-ss 3922  df-sn 4580  df-pr 4582  df-uni 4862

This theorem is referenced by:  unisnv  4881  unidif0  5302  op1sta  6178  op2nda  6181  opswap  6182  fvssunirnOLD  6858  funfv  6914  dffv2  6922  nlim1  8414  tc2  9657  cflim2  10176  fin1a2lem12  10324  acsmapd  18478  ghmqusnsglem1  19177  ghmquskerlem1  19180  pmtrprfval  19384  lspuni0  20931  lss0v  20938  zrhval2  21433  indistopon  22904  refun0  23418  qtopeu  23619  hmphindis  23700  filconn  23786  ufildr  23834  cnextfres1  23971  bday1s  27763  old1  27807  madeoldsuc  27817  zs12bday  28379  dimval  33572  dimvalfi  33573  locfinref  33807  pstmfval  33862  esumval  34012  esumpfinval  34041  esumpfinvalf  34042  prsiga  34097  carsggect  34285  indispconn  35206  onsucsuccmpi  36416  bj-nuliotaALT  37031  heiborlem3  37792  isomenndlem  46512  uniimaelsetpreimafv  47381