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

Theorem ssnid 4045
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 3109 . 2  |-  x  e. 
_V
21snid 4044 1  |-  x  e. 
{ x }
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1823   {csn 4016
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-v 3108  df-sn 4017
This theorem is referenced by:  exsnrex  4054  rext  4685  unipw  4687  xpdifid  5420  opabiota  5911  fnressn  6059  fressnfv  6061  snnex  6579  findcard2d  7754  ac6sfi  7756  iunfi  7800  elirrv  8015  kmlem2  8522  fin1a2lem10  8780  hsmexlem4  8800  iunfo  8905  fsumsplitsnun  13652  fsumcom2  13671  modfsummodslem1  13688  fprodcom2  13870  lbsextlem4  18002  coe1fzgsumdlem  18538  evl1gsumdlem  18587  frlmlbs  18999  maducoeval2  19309  dishaus  20050  dis2ndc  20127  dislly  20164  dissnlocfin  20196  comppfsc  20199  txdis  20299  txdis1cn  20302  txkgen  20319  isufil2  20575  alexsubALTlem4  20716  tmdgsum  20760  dscopn  21260  ovolfiniun  22078  volfiniun  22123  jensen  23516  cusgrares  24674  uvtx01vtx  24694  frgrancvvdeqlem3  25234  frgrancvvdeqlem4  25235  frgrawopreg1  25252  frgrawopreg2  25253  esum2dlem  28321  cvmlift2lem1  29011  wfrlem14  29596  wfrlem16  29598  funpartlem  29820  finixpnum  30278  mbfresfi  30301  mzpcompact2lem  30923  fourierdlem48  32176  c0snmgmhm  32974  bnj1498  34518  pclfinN  36021
  Copyright terms: Public domain W3C validator