Theorem unisnv 4927

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

Syntax hints:   = wceq 1542  {csn 4624  ∪ cuni 4904

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-un 3951  df-in 3953  df-ss 3963  df-sn 4625  df-pr 4627  df-uni 4905

This theorem is referenced by:  uniintsn  4987  uniabio  6502  iotauni2  6504  opabiotafun  6961  onuninsuci  7816  en1b  9011  fin1a2lem10  10391  incexclem  15769  sylow2a  19471  1stckgenlem  23026  alexsubALTlem3  23522  ptcmplem2  23526  icccmplem1  24307  unidifsnel  31738  unidifsnne  31739  disjabrex  31779  disjabrexf  31780  fiunelcarsg  33246  carsgclctunlem1  33247  fobigcup  34803  mbfresfi  36439