Theorem unisnv 4896

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

Syntax hints:   = wceq 1567  {csn 4594  ∪ cuni 4876

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-v 3465  df-un 3918  df-ss 3930  df-sn 4595  df-pr 4597  df-uni 4877

This theorem is referenced by:  uniintsn  4954  uniabio  6507  iotauni2  6509  opabiotafun  6962  onuninsuci  7836  en1b  9022  fin1a2lem10  10393  incexclem  15890  sylow2a  19689  1stckgenlem  23679  alexsubALTlem3  24175  ptcmplem2  24179  icccmplem1  24949  unidifsnel  32822  unidifsnne  32823  disjabrex  32868  disjabrexf  32869  esplyfval1  33908  fiunelcarsg  34651  carsgclctunlem1  34652  fineqvnttrclselem2  35458  fineqvnttrclse  35460  wevgblacfn  35494  fobigcup  36289  mbfresfi  38205  termco  50144