Theorem unisnv 4951

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

Syntax hints:   = wceq 1537  {csn 4648  ∪ cuni 4931

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-v 3490  df-un 3981  df-ss 3993  df-sn 4649  df-pr 4651  df-uni 4932

This theorem is referenced by:  uniintsn  5009  uniabio  6540  iotauni2  6542  opabiotafun  7002  onuninsuci  7877  en1b  9088  fin1a2lem10  10478  incexclem  15884  sylow2a  19661  1stckgenlem  23582  alexsubALTlem3  24078  ptcmplem2  24082  icccmplem1  24863  unidifsnel  32563  unidifsnne  32564  disjabrex  32604  disjabrexf  32605  fiunelcarsg  34281  carsgclctunlem1  34282  wevgblacfn  35076  fobigcup  35864  mbfresfi  37626