Theorem vsnid 4602

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

Assertion

Ref	Expression
vsnid	⊢ 𝑥 ∈ {𝑥}

Proof of Theorem vsnid

Step	Hyp	Ref	Expression
1		vex 3497	. 2 ⊢ 𝑥 ∈ V
2	1	snid 4601	1 ⊢ 𝑥 ∈ {𝑥}

Syntax hints:   ∈ wcel 2114  {csn 4567

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-v 3496  df-sn 4568

This theorem is referenced by:  exsnrex  4618  rext  5341  unipw  5343  xpdifid  6025  opabiota  6746  fnressn  6920  fressnfv  6922  snnex  7480  wfrlem14  7968  wfrlem16  7970  mapsnd  8450  findcard2d  8760  ac6sfi  8762  iunfi  8812  elirrv  9060  kmlem2  9577  fin1a2lem10  9831  hsmexlem4  9851  iunfo  9961  modfsummodslem1  15147  lcmfunsnlem2lem1  15982  coprmprod  16005  coprmproddvdslem  16006  lbsextlem4  19933  coe1fzgsumdlem  20469  evl1gsumdlem  20519  frlmlbs  20941  maducoeval2  21249  dishaus  21990  dis2ndc  22068  dislly  22105  dissnlocfin  22137  comppfsc  22140  txdis  22240  txdis1cn  22243  txkgen  22260  isufil2  22516  alexsubALTlem4  22658  tmdgsum  22703  dscopn  23183  ovolfiniun  24102  volfiniun  24148  jensen  25566  uvtx01vtx  27179  cplgr1vlem  27211  unidifsnel  30295  extdg1id  31053  esum2dlem  31351  bnj1498  32333  funen1cnv  32357  cvmlift2lem1  32549  frrlem12  33134  frrlem14  33136  funpartlem  33403  topdifinffinlem  34631  fvineqsneq  34696  pibt2  34701  finixpnum  34892  mbfresfi  34953  pclfinN  37051  mzpcompact2lem  39368  fourierdlem48  42459  sge0sup  42693  funressnvmo  43300  c0snmgmhm  44205