Theorem unisnv 4876

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

Syntax hints:   = wceq 1541  {csn 4573  ∪ cuni 4856

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-v 3438  df-un 3902  df-ss 3914  df-sn 4574  df-pr 4576  df-uni 4857

This theorem is referenced by:  uniintsn  4933  uniabio  6451  iotauni2  6453  opabiotafun  6902  onuninsuci  7770  en1b  8947  fin1a2lem10  10300  incexclem  15743  sylow2a  19531  1stckgenlem  23468  alexsubALTlem3  23964  ptcmplem2  23968  icccmplem1  24738  unidifsnel  32515  unidifsnne  32516  disjabrex  32562  disjabrexf  32563  fiunelcarsg  34329  carsgclctunlem1  34330  fineqvnttrclselem2  35142  fineqvnttrclse  35144  wevgblacfn  35153  fobigcup  35942  mbfresfi  37716  termco  49592