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  19533  1stckgenlem  23473  alexsubALTlem3  23969  ptcmplem2  23973  icccmplem1  24744  unidifsnel  32514  unidifsnne  32515  disjabrex  32561  disjabrexf  32562  fiunelcarsg  34300  carsgclctunlem1  34301  wevgblacfn  35089  fobigcup  35881  mbfresfi  37653  termco  49463