Theorem vsnid 4156

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

Assertion

Ref	Expression
vsnid	⊢ 𝑥 ∈ {𝑥}

Proof of Theorem vsnid

Step	Hyp	Ref	Expression
1		vex 3176	. 2 ⊢ 𝑥 ∈ V
2	1	snid 4155	1 ⊢ 𝑥 ∈ {𝑥}

Syntax hints:   ∈ wcel 1977  {csn 4125

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-v 3175  df-sn 4126

This theorem is referenced by:  exsnrex  4168  rext  4843  unipw  4845  xpdifid  5481  opabiota  6171  fnressn  6330  fressnfv  6332  snnex  6862  wfrlem14  7315  wfrlem16  7317  findcard2d  8087  ac6sfi  8089  iunfi  8137  elirrv  8387  kmlem2  8856  fin1a2lem10  9114  hsmexlem4  9134  iunfo  9240  fsumsplitsnun  14328  fsumcom2OLD  14348  modfsummodslem1  14365  fprodcom2OLD  14554  lcmfunsnlem2lem1  15189  coprmprod  15213  coprmproddvdslem  15214  lbsextlem4  18982  coe1fzgsumdlem  19492  evl1gsumdlem  19541  frlmlbs  19955  maducoeval2  20265  dishaus  20996  dis2ndc  21073  dislly  21110  dissnlocfin  21142  comppfsc  21145  txdis  21245  txdis1cn  21248  txkgen  21265  isufil2  21522  alexsubALTlem4  21664  tmdgsum  21709  dscopn  22188  ovolfiniun  23076  volfiniun  23122  jensen  24515  cusgrares  26001  uvtx01vtx  26020  frgrancvvdeqlem3  26559  frgrancvvdeqlem4  26560  frgrawopreg1  26577  frgrawopreg2  26578  esum2dlem  29481  bnj1498  30383  cvmlift2lem1  30538  funpartlem  31219  topdifinffinlem  32371  finixpnum  32564  mbfresfi  32626  pclfinN  34204  mzpcompact2lem  36332  fourierdlem48  39047  sge0sup  39284  uvtxa01vtx0  40623  cplgr1vlem  40651  frgrncvvdeqlem3  41471  frgrncvvdeqlem4  41472  frgrwopreg1  41487  frgrwopreg2  41488  c0snmgmhm  41704