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

Proof of Theorem vsnid
StepHypRef Expression
1 vex 2689 . 2
21snid 3556 1
 Colors of variables: wff set class Syntax hints:   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