Theorem unisn 4893

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

Syntax hints:   = wceq 1540   ∈ wcel 2109  Vcvv 3450  {csn 4592  ∪ cuni 4874

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 2702

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 2709  df-cleq 2722  df-clel 2804  df-v 3452  df-un 3922  df-ss 3934  df-sn 4593  df-pr 4595  df-uni 4875

This theorem is referenced by:  unisnv  4894  unidif0  5318  op1sta  6201  op2nda  6204  opswap  6205  fvssunirnOLD  6895  funfv  6951  dffv2  6959  nlim1  8456  tc2  9702  cflim2  10223  fin1a2lem12  10371  acsmapd  18520  ghmqusnsglem1  19219  ghmquskerlem1  19222  pmtrprfval  19424  lspuni0  20923  lss0v  20930  zrhval2  21425  indistopon  22895  refun0  23409  qtopeu  23610  hmphindis  23691  filconn  23777  ufildr  23825  cnextfres1  23962  bday1s  27750  old1  27794  madeoldsuc  27803  zs12bday  28350  dimval  33603  dimvalfi  33604  locfinref  33838  pstmfval  33893  esumval  34043  esumpfinval  34072  esumpfinvalf  34073  prsiga  34128  carsggect  34316  indispconn  35228  onsucsuccmpi  36438  bj-nuliotaALT  37053  heiborlem3  37814  isomenndlem  46535  uniimaelsetpreimafv  47401