Theorem unisnv 4878

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

Syntax hints:   = wceq 1540  {csn 4577  ∪ cuni 4858

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3438  df-un 3908  df-ss 3920  df-sn 4578  df-pr 4580  df-uni 4859

This theorem is referenced by:  uniintsn  4935  uniabio  6452  iotauni2  6454  opabiotafun  6903  onuninsuci  7773  en1b  8950  fin1a2lem10  10303  incexclem  15743  sylow2a  19498  1stckgenlem  23438  alexsubALTlem3  23934  ptcmplem2  23938  icccmplem1  24709  unidifsnel  32479  unidifsnne  32480  disjabrex  32526  disjabrexf  32527  fiunelcarsg  34284  carsgclctunlem1  34285  fineqvnttrclselem2  35075  fineqvnttrclse  35077  wevgblacfn  35086  fobigcup  35878  mbfresfi  37650  termco  49470