Theorem unisnv 4885

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

Syntax hints:   = wceq 1560  {csn 4582  ∪ cuni 4865

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-tru 1563  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837  df-v 3456  df-un 3909  df-ss 3921  df-sn 4583  df-pr 4585  df-uni 4866

This theorem is referenced by:  uniintsn  4943  uniabio  6491  iotauni2  6493  opabiotafun  6947  onuninsuci  7820  en1b  9006  fin1a2lem10  10366  incexclem  15866  sylow2a  19659  1stckgenlem  23613  alexsubALTlem3  24109  ptcmplem2  24113  icccmplem1  24883  unidifsnel  32734  unidifsnne  32735  disjabrex  32782  disjabrexf  32783  esplyfval1  33870  fiunelcarsg  34613  carsgclctunlem1  34614  fineqvnttrclselem2  35418  fineqvnttrclse  35420  wevgblacfn  35454  fobigcup  36248  mbfresfi  38165  termco  50102