Theorem ssnid 4058

Description: A setvar variable is a member of its singleton (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)

Assertion

Ref	Expression
ssnid

Proof of Theorem ssnid

Step	Hyp	Ref	Expression
1		vex 3112	. 2
2	1	snid 4057	1

Syntax hints:  e.wcel 1818  {csn 4029

This theorem is referenced by:  exsnrex  4067  rext  4700  unipw  4702  xpdifid  5440  opabiota  5936  fnressn  6083  fressnfv  6085  snnex  6606  findcard2d  7782  ac6sfi  7784  iunfi  7828  elirrv  8044  kmlem2  8552  fin1a2lem10  8810  hsmexlem4  8830  iunfo  8935  fsumsplitsnun  13570  fsumcom2  13589  modfsummodslem1  13606  fprodcom2  13788  lbsextlem4  17807  coe1fzgsumdlem  18343  evl1gsumdlem  18392  frlmlbs  18831  maducoeval2  19142  dishaus  19883  dis2ndc  19961  dislly  19998  dissnlocfin  20030  comppfsc  20033  txdis  20133  txdis1cn  20136  txkgen  20153  isufil2  20409  alexsubALTlem4  20550  tmdgsum  20594  dscopn  21094  ovolfiniun  21912  volfiniun  21957  jensen  23318  cusgrares  24472  uvtx01vtx  24492  frgrancvvdeqlem3  25032  frgrancvvdeqlem4  25033  frgrawopreg1  25050  frgrawopreg2  25051  cvmlift2lem1  28747  wfrlem14  29356  wfrlem16  29358  funpartlem  29592  finixpnum  30038  mbfresfi  30061  mzpcompact2lem  30684  fourierdlem48  31937  c0snmgmhm  32720  bnj1498  34117  pclfinN  35624

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-v 3111  df-sn 4030