Theorem unisnv 4908

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

Syntax hints:   = wceq 1540  {csn 4606  ∪ cuni 4888

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2715  df-cleq 2728  df-clel 2810  df-v 3466  df-un 3936  df-ss 3948  df-sn 4607  df-pr 4609  df-uni 4889

This theorem is referenced by:  uniintsn  4966  uniabio  6503  iotauni2  6505  opabiotafun  6964  onuninsuci  7840  en1b  9044  fin1a2lem10  10428  incexclem  15857  sylow2a  19605  1stckgenlem  23496  alexsubALTlem3  23992  ptcmplem2  23996  icccmplem1  24767  unidifsnel  32521  unidifsnne  32522  disjabrex  32568  disjabrexf  32569  fiunelcarsg  34353  carsgclctunlem1  34354  wevgblacfn  35136  fobigcup  35923  mbfresfi  37695