Theorem unisn 4884

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

Syntax hints:   = wceq 1542   ∈ wcel 2114  Vcvv 3442  {csn 4582  ∪ cuni 4865

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3444  df-un 3908  df-ss 3920  df-sn 4583  df-pr 4585  df-uni 4866

This theorem is referenced by:  unisnv  4885  unidif0  5307  op1sta  6191  op2nda  6194  opswap  6195  funfv  6929  dffv2  6937  nlim1  8426  tc2  9661  cflim2  10185  fin1a2lem12  10333  acsmapd  18489  ghmqusnsglem1  19221  ghmquskerlem1  19224  pmtrprfval  19428  lspuni0  20973  lss0v  20980  zrhval2  21475  indistopon  22957  refun0  23471  qtopeu  23672  hmphindis  23753  filconn  23839  ufildr  23887  cnextfres1  24024  bday1  27822  old1  27873  madeoldsuc  27893  dimval  33777  dimvalfi  33778  locfinref  34018  pstmfval  34073  esumval  34223  esumpfinval  34252  esumpfinvalf  34253  prsiga  34308  carsggect  34495  fineqvnttrclse  35299  indispconn  35447  onsucsuccmpi  36656  bj-nuliotaALT  37300  heiborlem3  38058  isomenndlem  46882  uniimaelsetpreimafv  47750