Theorem unisn 4858

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

Syntax hints:   = wceq 1539   ∈ wcel 2108  Vcvv 3422  {csn 4558  ∪ cuni 4836

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-un 3888  df-in 3890  df-ss 3900  df-sn 4559  df-pr 4561  df-uni 4837

This theorem is referenced by:  uniintsn  4915  unidif0  5277  op1sta  6117  op2nda  6120  opswap  6121  unisuc  6327  uniabio  6391  fvssunirn  6785  opabiotafun  6831  funfv  6837  dffv2  6845  onuninsuci  7662  en1b  8767  en1bOLD  8768  tc2  9431  cflim2  9950  fin1a2lem10  10096  fin1a2lem12  10098  incexclem  15476  acsmapd  18187  pmtrprfval  19010  sylow2a  19139  lspuni0  20187  lss0v  20193  zrhval2  20622  indistopon  22059  refun0  22574  1stckgenlem  22612  qtopeu  22775  hmphindis  22856  filconn  22942  ufildr  22990  alexsubALTlem3  23108  ptcmplem2  23112  cnextfres1  23127  icccmplem1  23891  unidifsnel  30784  unidifsnne  30785  disjabrex  30822  disjabrexf  30823  dimval  31588  dimvalfi  31589  locfinref  31693  pstmfval  31748  esumval  31914  esumpfinval  31943  esumpfinvalf  31944  prsiga  31999  fiunelcarsg  32183  carsgclctunlem1  32184  carsggect  32185  indispconn  33096  bday1s  33952  madeoldsuc  33994  fobigcup  34129  onsucsuccmpi  34559  bj-nuliotaALT  35156  mbfresfi  35750  heiborlem3  35898  sn-iotauni  40120  isomenndlem  43958  uniimaelsetpreimafv  44736