Theorem unisn 4931

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

Syntax hints:   = wceq 1542   ∈ wcel 2107  Vcvv 3475  {csn 4629  ∪ cuni 4909

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-un 3954  df-in 3956  df-ss 3966  df-sn 4630  df-pr 4632  df-uni 4910

This theorem is referenced by:  unisnv  4932  unidif0  5359  op1sta  6225  op2nda  6228  opswap  6229  fvssunirnOLD  6926  funfv  6979  dffv2  6987  nlim1  8489  en1bOLD  9024  tc2  9737  cflim2  10258  fin1a2lem12  10406  acsmapd  18507  pmtrprfval  19355  lspuni0  20621  lss0v  20627  zrhval2  21058  indistopon  22504  refun0  23019  qtopeu  23220  hmphindis  23301  filconn  23387  ufildr  23435  cnextfres1  23572  bday1s  27332  old1  27370  madeoldsuc  27379  ghmquskerlem1  32528  dimval  32686  dimvalfi  32687  locfinref  32821  pstmfval  32876  esumval  33044  esumpfinval  33073  esumpfinvalf  33074  prsiga  33129  carsggect  33317  indispconn  34225  onsucsuccmpi  35328  bj-nuliotaALT  35939  heiborlem3  36681  isomenndlem  45246  uniimaelsetpreimafv  46064