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

Theorem ssnid 3970
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 3025 . 2  |-  x  e. 
_V
21snid 3969 1  |-  x  e. 
{ x }
Colors of variables: wff setvar class
Syntax hints:    e. wcel 1872   {csn 3941
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2063  ax-ext 2408
This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2558  df-v 3024  df-sn 3942
This theorem is referenced by:  exsnrex  3980  rext  4612  unipw  4614  xpdifid  5227  opabiota  5888  fnressn  6035  fressnfv  6037  snnex  6555  wfrlem14  7004  wfrlem16  7006  findcard2d  7766  ac6sfi  7768  iunfi  7815  elirrv  8065  kmlem2  8532  fin1a2lem10  8790  hsmexlem4  8810  iunfo  8915  fsumsplitsnun  13759  fsumcom2  13778  modfsummodslem1  13795  fprodcom2  13981  lcmfunsnlem2lem1  14554  coprmprod  14621  coprmproddvdslem  14622  lbsextlem4  18327  coe1fzgsumdlem  18838  evl1gsumdlem  18887  frlmlbs  19297  maducoeval2  19607  dishaus  20340  dis2ndc  20417  dislly  20454  dissnlocfin  20486  comppfsc  20489  txdis  20589  txdis1cn  20592  txkgen  20609  isufil2  20865  alexsubALTlem4  21007  tmdgsum  21052  dscopn  21530  ovolfiniun  22396  volfiniun  22442  jensen  23856  cusgrares  25142  uvtx01vtx  25162  frgrancvvdeqlem3  25702  frgrancvvdeqlem4  25703  frgrawopreg1  25720  frgrawopreg2  25721  esum2dlem  28865  bnj1498  29822  cvmlift2lem1  29977  funpartlem  30658  topdifinffinlem  31657  finixpnum  31837  mbfresfi  31894  pclfinN  33377  mzpcompact2lem  35505  fourierdlem48  37901  sge0sup  38084  uvtxa01vtx0  39199  c0snmgmhm  39505
  Copyright terms: Public domain W3C validator