Theorem unisnv 4894

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

This proof depends on syntax axioms:   = wceq 1570  {csn 4591  ∪ cuni 4874

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 2148  ax-9 2156  ax-ext 2737

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 2744  df-cleq 2757  df-clel 2840  df-v 3459  df-un 3911  df-ss 3923  df-sn 4592  df-pr 4594  df-uni 4875

This theorem is used by:  uniintsn  4952  uniabio  6510  iotauni2  6512  opabiotafun  6965  onuninsuci  7842  en1b  9028  fin1a2lem10  10408  incexclem  15915  sylow2a  19735  1stckgenlem  23763  alexsubALTlem3  24259  ptcmplem2  24263  icccmplem1  25033  unidifsnel  32954  unidifsnne  32955  disjabrex  33000  disjabrexf  33001  esplyfval1  34029  fiunelcarsg  34773  carsgclctunlem1  34774  fineqvnttrclselem2  35594  fineqvnttrclse  35596  wevgblacfn  35654  fobigcup  36429  mbfresfi  38376  termco  50318