Theorem vsnid 4554

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

Syntax hints:   ∈ wcel 2113  {csn 4517

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1916  ax-6 1974  ax-7 2019  ax-8 2115  ax-9 2123  ax-ext 2710

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1545  df-ex 1787  df-sb 2074  df-clab 2717  df-cleq 2730  df-clel 2811  df-v 3400  df-sn 4518

This theorem is referenced by:  exsnrex  4572  rext  5308  unipw  5310  xpdifid  6001  opabiota  6752  fnressn  6931  fressnfv  6933  snnex  7500  wfrlem14  7998  wfrlem16  8000  mapsnd  8497  findcard2d  8766  ac6sfi  8837  iunfi  8886  elirrv  9134  kmlem2  9652  fin1a2lem10  9910  hsmexlem4  9930  iunfo  10040  modfsummodslem1  15241  lcmfunsnlem2lem1  16080  coprmprod  16103  coprmproddvdslem  16104  lbsextlem4  20053  frlmlbs  20614  coe1fzgsumdlem  21077  evl1gsumdlem  21127  maducoeval2  21392  dishaus  22134  dis2ndc  22212  dislly  22249  dissnlocfin  22281  comppfsc  22284  txdis  22384  txdis1cn  22387  txkgen  22404  isufil2  22660  alexsubALTlem4  22802  tmdgsum  22847  dscopn  23327  ovolfiniun  24254  volfiniun  24300  jensen  25726  uvtx01vtx  27339  cplgr1vlem  27371  unidifsnel  30457  gsumpart  30892  extdg1id  31310  esum2dlem  31630  bnj1498  32612  funen1cnv  32631  cvmlift2lem1  32835  frrlem12  33452  frrlem14  33454  funpartlem  33882  topdifinffinlem  35138  fvineqsneq  35203  pibt2  35208  finixpnum  35382  mbfresfi  35443  pclfinN  37534  mzpcompact2lem  40137  fourierdlem48  43229  sge0sup  43463  funressnvmo  44070  c0snmgmhm  44998