Theorem unisn 4827

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

Syntax hints:   = wceq 1543   ∈ wcel 2112  Vcvv 3398  {csn 4527  ∪ cuni 4805

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-8 2114  ax-9 2122  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-tru 1546  df-ex 1788  df-sb 2073  df-clab 2715  df-cleq 2728  df-clel 2809  df-v 3400  df-un 3858  df-in 3860  df-ss 3870  df-sn 4528  df-pr 4530  df-uni 4806

This theorem is referenced by:  uniintsn  4884  unidif0  5236  op1sta  6068  op2nda  6071  opswap  6072  unisuc  6267  uniabio  6331  fvssunirn  6724  opabiotafun  6770  funfv  6776  dffv2  6784  onuninsuci  7597  en1b  8678  en1bOLD  8679  tc2  9336  cflim2  9842  fin1a2lem10  9988  fin1a2lem12  9990  incexclem  15363  acsmapd  18014  pmtrprfval  18833  sylow2a  18962  lspuni0  20001  lss0v  20007  zrhval2  20429  indistopon  21852  refun0  22366  1stckgenlem  22404  qtopeu  22567  hmphindis  22648  filconn  22734  ufildr  22782  alexsubALTlem3  22900  ptcmplem2  22904  cnextfres1  22919  icccmplem1  23673  unidifsnel  30556  unidifsnne  30557  disjabrex  30594  disjabrexf  30595  dimval  31354  dimvalfi  31355  locfinref  31459  pstmfval  31514  esumval  31680  esumpfinval  31709  esumpfinvalf  31710  prsiga  31765  fiunelcarsg  31949  carsgclctunlem1  31950  carsggect  31951  indispconn  32863  bday1s  33711  madeoldsuc  33753  fobigcup  33888  onsucsuccmpi  34318  bj-nuliotaALT  34915  mbfresfi  35509  heiborlem3  35657  isomenndlem  43686  uniimaelsetpreimafv  44464