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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3444  df-un 3908  df-ss 3920  df-sn 4583  df-pr 4585  df-uni 4866

This theorem is referenced by:  uniintsn  4942  uniabio  6470  iotauni2  6472  opabiotafun  6922  onuninsuci  7792  en1b  8974  fin1a2lem10  10331  incexclem  15771  sylow2a  19560  1stckgenlem  23509  alexsubALTlem3  24005  ptcmplem2  24009  icccmplem1  24779  unidifsnel  32622  unidifsnne  32623  disjabrex  32669  disjabrexf  32670  esplyfval1  33750  fiunelcarsg  34494  carsgclctunlem1  34495  fineqvnttrclselem2  35300  fineqvnttrclse  35302  wevgblacfn  35325  fobigcup  36114  mbfresfi  37917  termco  49840