Theorem unisnv 4887

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

Syntax hints:   = wceq 1540  {csn 4585  ∪ cuni 4867

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 3446  df-un 3916  df-ss 3928  df-sn 4586  df-pr 4588  df-uni 4868

This theorem is referenced by:  uniintsn  4945  uniabio  6466  iotauni2  6468  opabiotafun  6923  onuninsuci  7796  en1b  8973  fin1a2lem10  10338  incexclem  15778  sylow2a  19525  1stckgenlem  23416  alexsubALTlem3  23912  ptcmplem2  23916  icccmplem1  24687  unidifsnel  32437  unidifsnne  32438  disjabrex  32484  disjabrexf  32485  fiunelcarsg  34280  carsgclctunlem1  34281  wevgblacfn  35069  fobigcup  35861  mbfresfi  37633  termco  49443