Theorem unisnv 4881

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

Syntax hints:   = wceq 1541  {csn 4578  ∪ cuni 4861

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 2706

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 2713  df-cleq 2726  df-clel 2809  df-v 3440  df-un 3904  df-ss 3916  df-sn 4579  df-pr 4581  df-uni 4862

This theorem is referenced by:  uniintsn  4938  uniabio  6460  iotauni2  6462  opabiotafun  6912  onuninsuci  7780  en1b  8960  fin1a2lem10  10317  incexclem  15757  sylow2a  19546  1stckgenlem  23495  alexsubALTlem3  23991  ptcmplem2  23995  icccmplem1  24765  unidifsnel  32559  unidifsnne  32560  disjabrex  32606  disjabrexf  32607  fiunelcarsg  34422  carsgclctunlem1  34423  fineqvnttrclselem2  35227  fineqvnttrclse  35229  wevgblacfn  35252  fobigcup  36041  mbfresfi  37806  termco  49668