Theorem unisnv 4858

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

Syntax hints:   = wceq 1547  {csn 4555  ∪ cuni 4838

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-v 3433  df-un 3888  df-ss 3900  df-sn 4556  df-pr 4558  df-uni 4839

This theorem is referenced by:  uniintsn  4915  uniabio  6455  iotauni2  6457  opabiotafun  6907  onuninsuci  7780  en1b  8962  fin1a2lem10  10322  incexclem  15792  sylow2a  19585  1stckgenlem  23536  alexsubALTlem3  24032  ptcmplem2  24036  icccmplem1  24806  unidifsnel  32623  unidifsnne  32624  disjabrex  32671  disjabrexf  32672  esplyfval1  33757  fiunelcarsg  34500  carsgclctunlem1  34501  fineqvnttrclselem2  35303  fineqvnttrclse  35305  wevgblacfn  35337  fobigcup  36126  mbfresfi  38033  termco  49971