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

This proof depends on syntax axioms:   = wceq 1570  {csn 4584  ∪ cuni 4867

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-un 3904  df-ss 3916  df-sn 4585  df-pr 4587  df-uni 4868

This theorem is used by:  uniintsn  4945  uniabio  6503  iotauni2  6505  opabiotafun  6959  onuninsuci  7837  en1b  9034  fin1a2lem10  10414  incexclem  15928  sylow2a  19749  1stckgenlem  23782  alexsubALTlem3  24278  ptcmplem2  24282  icccmplem1  25052  unidifsnel  33013  unidifsnne  33014  disjabrex  33058  disjabrexf  33059  esplyfval1  34086  fiunelcarsg  34830  carsgclctunlem1  34831  fineqvnttrclselem2  35651  fineqvnttrclse  35653  wevgblacfn  35711  fobigcup  36480  mbfresfi  38418  termco  50410