Theorem vsnid 4622

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

Syntax hints:   ∈ wcel 2114  {csn 4582

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3444  df-sn 4583

This theorem is referenced by:  exsnrex  4639  rext  5405  unipw  5407  xpdifid  6136  opabiota  6926  fnressn  7115  fressnfv  7117  snnex  7715  frrlem12  8251  frrlem14  8253  mapsnd  8838  findcard2d  9105  ac6sfi  9198  iunfi  9257  elirrvOLD  9517  kmlem2  10076  fin1a2lem10  10333  hsmexlem4  10353  iunfo  10463  modfsummodslem1  15729  lcmfunsnlem2lem1  16579  coprmprod  16602  coprmproddvdslem  16603  c0snmgmhm  20415  lbsextlem4  21133  frlmlbs  21769  coe1fzgsumdlem  22264  evl1gsumdlem  22317  maducoeval2  22601  dishaus  23343  dis2ndc  23421  dislly  23458  dissnlocfin  23490  comppfsc  23493  txdis  23593  txdis1cn  23596  txkgen  23613  isufil2  23869  alexsubALTlem4  24011  tmdgsum  24056  dscopn  24534  ovolfiniun  25475  volfiniun  25521  jensen  26972  uvtx01vtx  29488  cplgr1vlem  29520  unidifsnel  32628  gsumpart  33163  vieta  33763  extdg1id  33850  irngss  33871  esum2dlem  34276  bnj1498  35243  funen1cnv  35271  fineqvnttrclselem2  35306  wevgblacfn  35331  cvmlift2lem1  35524  funpartlem  36164  exeltr  36693  topdifinffinlem  37629  fvineqsneq  37694  pibt2  37699  finixpnum  37885  mbfresfi  37946  pclfinN  40305  sn-iotalem  42622  mzpcompact2lem  43137  dvmptfprod  46332  fourierdlem48  46541  sge0sup  46778  funressnvmo  47434  dfclnbgr6  48245  dfsclnbgr6  48247  termco  49869  termcarweu  49916  diag1f1o  49922  diag2f1o  49925