ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  vsnid Unicode version

Theorem vsnid 3557
Description: A setvar variable is a member of its singleton (common case). (Contributed by David A. Wheeler, 8-Dec-2018.)
Assertion
Ref Expression
vsnid  |-  x  e. 
{ x }

Proof of Theorem vsnid
StepHypRef Expression
1 vex 2689 . 2  |-  x  e. 
_V
21snid 3556 1  |-  x  e. 
{ x }
Colors of variables: wff set class
Syntax hints:    e. wcel 1480   {csn 3527
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 698  ax-5 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-10 1483  ax-11 1484  ax-i12 1485  ax-bndl 1486  ax-4 1487  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2121
This theorem depends on definitions:  df-bi 116  df-tru 1334  df-nf 1437  df-sb 1736  df-clab 2126  df-cleq 2132  df-clel 2135  df-nfc 2270  df-v 2688  df-sn 3533
This theorem is referenced by:  rext  4137  snnex  4369  dtruex  4474  fnressn  5606  fressnfv  5607  findcard2d  6785  findcard2sd  6786  diffifi  6788  ac6sfi  6792  fisseneq  6820  finomni  7012  cc2lem  7086  modfsummodlem1  11237  txdis  12460  txdis1cn  12461
  Copyright terms: Public domain W3C validator