![]() |
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 3343 | . 2 ⊢ 𝑥 ∈ V | |
2 | 1 | snid 4353 | 1 ⊢ 𝑥 ∈ {𝑥} |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2139 {csn 4321 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1871 ax-4 1886 ax-5 1988 ax-6 2054 ax-7 2090 ax-9 2148 ax-10 2168 ax-11 2183 ax-12 2196 ax-13 2391 ax-ext 2740 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-tru 1635 df-ex 1854 df-nf 1859 df-sb 2047 df-clab 2747 df-cleq 2753 df-clel 2756 df-nfc 2891 df-v 3342 df-sn 4322 |
This theorem is referenced by: exsnrex 4365 rext 5065 unipw 5067 xpdifid 5720 opabiota 6423 fnressn 6588 fressnfv 6590 snnex 7131 snnexOLD 7132 wfrlem14 7597 wfrlem16 7599 findcard2d 8367 ac6sfi 8369 iunfi 8419 elirrv 8666 kmlem2 9165 fin1a2lem10 9423 hsmexlem4 9443 iunfo 9553 fsumsplitsnunOLD 14685 fsumcom2OLD 14705 modfsummodslem1 14723 fprodcom2OLD 14914 lcmfunsnlem2lem1 15553 coprmprod 15577 coprmproddvdslem 15578 lbsextlem4 19363 coe1fzgsumdlem 19873 evl1gsumdlem 19922 frlmlbs 20338 maducoeval2 20648 dishaus 21388 dis2ndc 21465 dislly 21502 dissnlocfin 21534 comppfsc 21537 txdis 21637 txdis1cn 21640 txkgen 21657 isufil2 21913 alexsubALTlem4 22055 tmdgsum 22100 dscopn 22579 ovolfiniun 23469 volfiniun 23515 jensen 24914 uvtx01vtx 26500 uvtxa01vtx0OLD 26502 cplgr1vlem 26535 esum2dlem 30463 bnj1498 31436 cvmlift2lem1 31591 funpartlem 32355 topdifinffinlem 33506 finixpnum 33707 mbfresfi 33769 pclfinN 35689 mzpcompact2lem 37816 fourierdlem48 40874 sge0sup 41111 c0snmgmhm 42424 |
Copyright terms: Public domain | W3C validator |