Theorem unisnv 4889

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

This proof depends on syntax axioms:   = wceq 1569  {csn 4587  ∪ cuni 4869

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-8 2148  ax-9 2156  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1572  df-ex 1812  df-sb 2101  df-clab 2742  df-cleq 2755  df-clel 2838  df-v 3455  df-ss 3900  df-un 4153  df-sn 4588  df-pr 4590  df-uni 4870

This theorem is used by:  uniintsn  4947  uniabio  6514  iotauni2  6516  opabiotafun  6973  onuninsuci  7858  en1b  9063  fin1a2lem10  10497  incexclem  16017  sylow2a  19845  1stckgenlem  23884  alexsubALTlem3  24380  ptcmplem2  24384  icccmplem1  25154  unidifsnel  33185  unidifsnne  33186  disjabrex  33230  disjabrexf  33231  esplyfval1  34258  fiunelcarsg  35001  carsgclctunlem1  35002  fineqvnttrclselem2  35861  fineqvnttrclse  35863  wevgblacfn  35993  fobigcup  36789  mbfresfi  38724  termco  50755