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 3441	. 2 ⊢ 𝑥 ∈ V
2	1	snid 4601	1 ⊢ 𝑥 ∈ {𝑥}

Syntax hints:   ∈ wcel 2104  {csn 4565

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2707

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1542  df-ex 1780  df-sb 2066  df-clab 2714  df-cleq 2728  df-clel 2814  df-v 3439  df-sn 4566

This theorem is referenced by:  exsnrex  4620  rext  5377  unipw  5379  xpdifid  6086  opabiota  6883  fnressn  7062  fressnfv  7064  snnex  7640  frrlem12  8144  frrlem14  8146  wfrlem14OLD  8184  wfrlem16OLD  8186  mapsnd  8705  findcard2d  8987  ac6sfi  9102  iunfi  9151  elirrv  9399  kmlem2  9953  fin1a2lem10  10211  hsmexlem4  10231  iunfo  10341  modfsummodslem1  15549  lcmfunsnlem2lem1  16388  coprmprod  16411  coprmproddvdslem  16412  lbsextlem4  20468  frlmlbs  21049  coe1fzgsumdlem  21517  evl1gsumdlem  21567  maducoeval2  21834  dishaus  22578  dis2ndc  22656  dislly  22693  dissnlocfin  22725  comppfsc  22728  txdis  22828  txdis1cn  22831  txkgen  22848  isufil2  23104  alexsubALTlem4  23246  tmdgsum  23291  dscopn  23774  ovolfiniun  24710  volfiniun  24756  jensen  26183  uvtx01vtx  27809  cplgr1vlem  27841  unidifsnel  30928  gsumpart  31360  extdg1id  31783  esum2dlem  32105  bnj1498  33086  funen1cnv  33105  cvmlift2lem1  33309  funpartlem  34289  topdifinffinlem  35562  fvineqsneq  35627  pibt2  35632  finixpnum  35806  mbfresfi  35867  pclfinN  37956  sn-iotalem  40232  mzpcompact2lem  40610  fourierdlem48  43744  sge0sup  43979  funressnvmo  44597  c0snmgmhm  45530