Theorem unisnv 4871

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

Syntax hints:   = wceq 1542  {csn 4568  ∪ cuni 4851

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 3432  df-un 3895  df-ss 3907  df-sn 4569  df-pr 4571  df-uni 4852

This theorem is referenced by:  uniintsn  4928  uniabio  6463  iotauni2  6465  opabiotafun  6915  onuninsuci  7785  en1b  8966  fin1a2lem10  10325  incexclem  15795  sylow2a  19588  1stckgenlem  23531  alexsubALTlem3  24027  ptcmplem2  24031  icccmplem1  24801  unidifsnel  32623  unidifsnne  32624  disjabrex  32670  disjabrexf  32671  esplyfval1  33735  fiunelcarsg  34479  carsgclctunlem1  34480  fineqvnttrclselem2  35285  fineqvnttrclse  35287  wevgblacfn  35310  fobigcup  36099  mbfresfi  38004  termco  49971