MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  unisnv Structured version   Visualization version   GIF version

Theorem unisnv 4927
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
StepHypRef Expression
1 vex 3479 . 2 𝑥 ∈ V
21unisn 4926 1 {𝑥} = 𝑥
Colors of variables: wff setvar class
Syntax hints:   = wceq 1542  {csn 4624   cuni 4904
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-un 3951  df-in 3953  df-ss 3963  df-sn 4625  df-pr 4627  df-uni 4905
This theorem is referenced by:  uniintsn  4987  uniabio  6502  iotauni2  6504  opabiotafun  6961  onuninsuci  7816  en1b  9011  fin1a2lem10  10391  incexclem  15769  sylow2a  19471  1stckgenlem  23026  alexsubALTlem3  23522  ptcmplem2  23526  icccmplem1  24307  unidifsnel  31738  unidifsnne  31739  disjabrex  31779  disjabrexf  31780  fiunelcarsg  33246  carsgclctunlem1  33247  fobigcup  34803  mbfresfi  36439
  Copyright terms: Public domain W3C validator