Theorem unisnv 4870

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 3433	. 2 ⊢ 𝑥 ∈ V
2	1	unisn 4869	1 ⊢ ∪ {𝑥} = 𝑥

Syntax hints:   = wceq 1542  {csn 4567  ∪ cuni 4850

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 2708

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 2715  df-cleq 2728  df-clel 2811  df-v 3431  df-un 3894  df-ss 3906  df-sn 4568  df-pr 4570  df-uni 4851

This theorem is referenced by:  uniintsn  4927  uniabio  6468  iotauni2  6470  opabiotafun  6920  onuninsuci  7791  en1b  8972  fin1a2lem10  10331  incexclem  15801  sylow2a  19594  1stckgenlem  23518  alexsubALTlem3  24014  ptcmplem2  24018  icccmplem1  24788  unidifsnel  32605  unidifsnne  32606  disjabrex  32652  disjabrexf  32653  esplyfval1  33717  fiunelcarsg  34460  carsgclctunlem1  34461  fineqvnttrclselem2  35266  fineqvnttrclse  35268  wevgblacfn  35291  fobigcup  36080  mbfresfi  37987  termco  49956