Theorem vsnid 3723

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

Assertion

Ref	Expression
vsnid	⊢ 𝑥 ∈ {𝑥}

Proof of Theorem vsnid

Step	Hyp	Ref	Expression
1		vex 2818	. 2 ⊢ 𝑥 ∈ V
2	1	snid 3722	1 ⊢ 𝑥 ∈ {𝑥}

Syntax hints:   ∈ wcel 2205  {csn 3691

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2216

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-nfc 2375  df-v 2817  df-sn 3697

This theorem is referenced by:  rext  4333  snnex  4571  dtruex  4683  fnressn  5872  fressnfv  5873  mapsnd  6925  findcard2d  7150  findcard2sd  7151  diffifi  7153  ac6sfi  7157  elssdc  7164  eqsndc  7165  fisseneq  7197  finomni  7433  cc2lem  7582  hashfibclem  11210  modfsummodlem1  12146  txdis  15159  txdis1cn  15160  gfsumz  16886  gfsumcl  16887