![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > vsnid | Structured version Visualization version GIF version |
Description: A setvar variable is a member of its singleton. (Contributed by David A. Wheeler, 8-Dec-2018.) |
Ref | Expression |
---|---|
vsnid | ⊢ 𝑥 ∈ {𝑥} |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | vex 3466 | . 2 ⊢ 𝑥 ∈ V | |
2 | 1 | snid 4669 | 1 ⊢ 𝑥 ∈ {𝑥} |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2099 {csn 4633 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2101 ax-9 2109 ax-ext 2697 |
This theorem depends on definitions: df-bi 206 df-an 395 df-tru 1537 df-ex 1775 df-sb 2061 df-clab 2704 df-cleq 2718 df-clel 2803 df-v 3464 df-sn 4634 |
This theorem is referenced by: exsnrex 4689 rext 5454 unipw 5456 xpdifid 6179 opabiota 6985 fnressn 7172 fressnfv 7174 snnex 7766 frrlem12 8312 frrlem14 8314 wfrlem14OLD 8352 wfrlem16OLD 8354 mapsnd 8915 findcard2d 9204 ac6sfi 9321 iunfi 9385 elirrv 9639 kmlem2 10194 fin1a2lem10 10452 hsmexlem4 10472 iunfo 10582 modfsummodslem1 15796 lcmfunsnlem2lem1 16639 coprmprod 16662 coprmproddvdslem 16663 c0snmgmhm 20444 lbsextlem4 21142 frlmlbs 21795 coe1fzgsumdlem 22294 evl1gsumdlem 22347 maducoeval2 22633 dishaus 23377 dis2ndc 23455 dislly 23492 dissnlocfin 23524 comppfsc 23527 txdis 23627 txdis1cn 23630 txkgen 23647 isufil2 23903 alexsubALTlem4 24045 tmdgsum 24090 dscopn 24573 ovolfiniun 25521 volfiniun 25567 jensen 27017 uvtx01vtx 29333 cplgr1vlem 29365 unidifsnel 32461 gsumpart 32923 extdg1id 33552 irngss 33563 esum2dlem 33925 bnj1498 34906 funen1cnv 34925 wevgblacfn 34936 cvmlift2lem1 35130 funpartlem 35766 topdifinffinlem 37054 fvineqsneq 37119 pibt2 37124 finixpnum 37306 mbfresfi 37367 pclfinN 39599 sn-iotalem 41943 mzpcompact2lem 42408 fourierdlem48 45775 sge0sup 46012 funressnvmo 46660 dfclnbgr6 47423 dfsclnbgr6 47425 |
Copyright terms: Public domain | W3C validator |