Theorem unisnv 4883

Description: A set equals the union of its singleton (setvar case). (Contributed by NM, 30-Aug-1993.)

Assertion

Ref	Expression
unisnv	⊢ ∪ {𝑥} = 𝑥

Proof of Theorem unisnv

Step	Hyp	Ref	Expression
1		vex 3444	. 2 ⊢ 𝑥 ∈ V
2	1	unisn 4882	1 ⊢ ∪ {𝑥} = 𝑥

Syntax hints:   = wceq 1541  {csn 4580  ∪ cuni 4863

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3442  df-un 3906  df-ss 3918  df-sn 4581  df-pr 4583  df-uni 4864

This theorem is referenced by:  uniintsn  4940  uniabio  6462  iotauni2  6464  opabiotafun  6914  onuninsuci  7782  en1b  8962  fin1a2lem10  10319  incexclem  15759  sylow2a  19548  1stckgenlem  23497  alexsubALTlem3  23993  ptcmplem2  23997  icccmplem1  24767  unidifsnel  32610  unidifsnne  32611  disjabrex  32657  disjabrexf  32658  fiunelcarsg  34473  carsgclctunlem1  34474  fineqvnttrclselem2  35278  fineqvnttrclse  35280  wevgblacfn  35303  fobigcup  36092  mbfresfi  37867  termco  49736