MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ssnid Structured version   Unicode version

Theorem ssnid 4043
Description: A setvar variable is a member of its singleton (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
Assertion
Ref Expression
ssnid  |-  x  e. 
{ x }

Proof of Theorem ssnid
StepHypRef Expression
1 vex 3098 . 2  |-  x  e. 
_V
21snid 4042 1  |-  x  e. 
{ x }
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1804   {csn 4014
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-v 3097  df-sn 4015
This theorem is referenced by:  exsnrex  4052  rext  4685  unipw  4687  xpdifid  5425  opabiota  5921  fnressn  6068  fressnfv  6070  snnex  6591  findcard2d  7764  ac6sfi  7766  iunfi  7810  elirrv  8026  kmlem2  8534  fin1a2lem10  8792  hsmexlem4  8812  iunfo  8917  fsumsplitsnun  13549  fsumcom2  13568  modfsummodslem1  13585  lbsextlem4  17681  coe1fzgsumdlem  18217  evl1gsumdlem  18266  frlmlbs  18704  maducoeval2  19015  dishaus  19756  dis2ndc  19834  dislly  19871  dissnlocfin  19903  comppfsc  19906  txdis  20006  txdis1cn  20009  txkgen  20026  isufil2  20282  alexsubALTlem4  20423  tmdgsum  20467  dscopn  20967  ovolfiniun  21785  volfiniun  21830  jensen  23190  cusgrares  24344  uvtx01vtx  24364  frgrancvvdeqlem3  24904  frgrancvvdeqlem4  24905  frgrawopreg1  24922  frgrawopreg2  24923  cvmlift2lem1  28620  fprodcom2  29089  wfrlem14  29331  wfrlem16  29333  funpartlem  29567  finixpnum  30013  mbfresfi  30036  mzpcompact2lem  30659  fourierdlem48  31826  bnj1498  33850  pclfinN  35364
  Copyright terms: Public domain W3C validator