Theorem unisnv 4909

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

Syntax hints:   = wceq 1539  {csn 4608  ∪ cuni 4889

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1542  df-ex 1779  df-sb 2064  df-clab 2713  df-cleq 2726  df-clel 2808  df-v 3466  df-un 3938  df-ss 3950  df-sn 4609  df-pr 4611  df-uni 4890

This theorem is referenced by:  uniintsn  4967  uniabio  6509  iotauni2  6511  opabiotafun  6970  onuninsuci  7844  en1b  9048  fin1a2lem10  10432  incexclem  15855  sylow2a  19610  1stckgenlem  23526  alexsubALTlem3  24022  ptcmplem2  24026  icccmplem1  24799  unidifsnel  32500  unidifsnne  32501  disjabrex  32542  disjabrexf  32543  fiunelcarsg  34259  carsgclctunlem1  34260  wevgblacfn  35055  fobigcup  35842  mbfresfi  37614