Theorem vsnid 4614

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

Syntax hints:   ∈ wcel 2110  {csn 4574

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 1968  ax-7 2009  ax-8 2112  ax-9 2120  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2067  df-clab 2709  df-cleq 2722  df-clel 2804  df-v 3436  df-sn 4575

This theorem is referenced by:  exsnrex  4631  rext  5387  unipw  5389  xpdifid  6112  opabiota  6899  fnressn  7086  fressnfv  7088  snnex  7686  frrlem12  8222  frrlem14  8224  mapsnd  8805  findcard2d  9071  ac6sfi  9163  iunfi  9222  elirrvOLD  9479  kmlem2  10035  fin1a2lem10  10292  hsmexlem4  10312  iunfo  10422  modfsummodslem1  15691  lcmfunsnlem2lem1  16541  coprmprod  16564  coprmproddvdslem  16565  c0snmgmhm  20373  lbsextlem4  21091  frlmlbs  21727  coe1fzgsumdlem  22211  evl1gsumdlem  22264  maducoeval2  22548  dishaus  23290  dis2ndc  23368  dislly  23405  dissnlocfin  23437  comppfsc  23440  txdis  23540  txdis1cn  23543  txkgen  23560  isufil2  23816  alexsubALTlem4  23958  tmdgsum  24003  dscopn  24481  ovolfiniun  25422  volfiniun  25468  jensen  26919  uvtx01vtx  29368  cplgr1vlem  29400  unidifsnel  32505  gsumpart  33027  extdg1id  33669  irngss  33690  esum2dlem  34095  bnj1498  35063  funen1cnv  35090  fineqvnttrclselem2  35110  wevgblacfn  35121  cvmlift2lem1  35314  funpartlem  35955  topdifinffinlem  37360  fvineqsneq  37425  pibt2  37430  finixpnum  37624  mbfresfi  37685  pclfinN  39918  sn-iotalem  42233  mzpcompact2lem  42763  dvmptfprod  45962  fourierdlem48  46171  sge0sup  46408  funressnvmo  47055  dfclnbgr6  47866  dfsclnbgr6  47868  termco  49492  termcarweu  49539  diag1f1o  49545  diag2f1o  49548