Theorem unisnv 4892

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

Syntax hints:   = wceq 1570  {csn 4589  ∪ cuni 4872

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-v 3457  df-un 3910  df-ss 3922  df-sn 4590  df-pr 4592  df-uni 4873

This theorem is referenced by:  uniintsn  4950  uniabio  6506  iotauni2  6508  opabiotafun  6961  onuninsuci  7832  en1b  9018  fin1a2lem10  10388  incexclem  15886  sylow2a  19684  1stckgenlem  23710  alexsubALTlem3  24206  ptcmplem2  24210  icccmplem1  24980  unidifsnel  32881  unidifsnne  32882  disjabrex  32927  disjabrexf  32928  esplyfval1  33963  fiunelcarsg  34706  carsgclctunlem1  34707  fineqvnttrclselem2  35535  fineqvnttrclse  35537  wevgblacfn  35595  fobigcup  36390  mbfresfi  38337  termco  50279