Theorem unisn 4930

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

Syntax hints:   = wceq 1542   ∈ wcel 2107  Vcvv 3475  {csn 4628  ∪ cuni 4908

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 3953  df-in 3955  df-ss 3965  df-sn 4629  df-pr 4631  df-uni 4909

This theorem is referenced by:  unisnv  4931  unidif0  5358  op1sta  6222  op2nda  6225  opswap  6226  fvssunirnOLD  6923  funfv  6976  dffv2  6984  nlim1  8486  en1bOLD  9021  tc2  9734  cflim2  10255  fin1a2lem12  10403  acsmapd  18504  pmtrprfval  19350  lspuni0  20614  lss0v  20620  zrhval2  21050  indistopon  22496  refun0  23011  qtopeu  23212  hmphindis  23293  filconn  23379  ufildr  23427  cnextfres1  23564  bday1s  27322  old1  27360  madeoldsuc  27369  ghmquskerlem1  32517  dimval  32675  dimvalfi  32676  locfinref  32810  pstmfval  32865  esumval  33033  esumpfinval  33062  esumpfinvalf  33063  prsiga  33118  carsggect  33306  indispconn  34214  onsucsuccmpi  35317  bj-nuliotaALT  35928  heiborlem3  36670  isomenndlem  45233  uniimaelsetpreimafv  46051