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 3455	. 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 2733

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 2740  df-cleq 2753  df-clel 2836  df-v 3453  df-un 3904  df-ss 3916  df-sn 4585  df-pr 4587  df-uni 4868

This theorem is used by:  uniintsn  4945  uniabio  6508  iotauni2  6510  opabiotafun  6965  onuninsuci  7851  en1b  9052  fin1a2lem10  10487  incexclem  16005  sylow2a  19833  1stckgenlem  23872  alexsubALTlem3  24368  ptcmplem2  24372  icccmplem1  25142  unidifsnel  33131  unidifsnne  33132  disjabrex  33176  disjabrexf  33177  esplyfval1  34205  fiunelcarsg  34948  carsgclctunlem1  34949  fineqvnttrclselem2  35790  fineqvnttrclse  35792  wevgblacfn  35890  fobigcup  36662  mbfresfi  38584  termco  50588