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 1537   ∈ wcel 2114  Vcvv 3494  {csn 4567  ∪ cuni 4838

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-v 3496  df-un 3941  df-in 3943  df-ss 3952  df-sn 4568  df-pr 4570  df-uni 4839

This theorem is referenced by:  uniintsn  4913  unidif0  5260  op1sta  6082  op2nda  6085  opswap  6086  unisuc  6267  uniabio  6328  fvssunirn  6699  opabiotafun  6744  funfv  6750  dffv2  6756  onuninsuci  7555  en1b  8577  tc2  9184  cflim2  9685  fin1a2lem10  9831  fin1a2lem12  9833  incexclem  15191  acsmapd  17788  pmtrprfval  18615  sylow2a  18744  lspuni0  19782  lss0v  19788  zrhval2  20656  indistopon  21609  refun0  22123  1stckgenlem  22161  qtopeu  22324  hmphindis  22405  filconn  22491  ufildr  22539  alexsubALTlem3  22657  ptcmplem2  22661  cnextfres1  22676  icccmplem1  23430  unidifsnel  30295  unidifsnne  30296  disjabrex  30332  disjabrexf  30333  dimval  31001  dimvalfi  31002  locfinref  31105  pstmfval  31136  esumval  31305  esumpfinval  31334  esumpfinvalf  31335  prsiga  31390  fiunelcarsg  31574  carsgclctunlem1  31575  carsggect  31576  indispconn  32481  fobigcup  33361  onsucsuccmpi  33791  bj-nuliotaALT  34354  mbfresfi  34953  heiborlem3  35106  isomenndlem  42832  uniimaelsetpreimafv  43576