![]() |
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 3447 | . 2 ⊢ 𝑥 ∈ V | |
2 | 1 | snid 4620 | 1 ⊢ 𝑥 ∈ {𝑥} |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2106 {csn 4584 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-ext 2707 |
This theorem depends on definitions: df-bi 206 df-an 397 df-tru 1544 df-ex 1782 df-sb 2068 df-clab 2714 df-cleq 2728 df-clel 2814 df-v 3445 df-sn 4585 |
This theorem is referenced by: exsnrex 4639 rext 5403 unipw 5405 xpdifid 6118 opabiota 6921 fnressn 7100 fressnfv 7102 snnex 7688 frrlem12 8224 frrlem14 8226 wfrlem14OLD 8264 wfrlem16OLD 8266 mapsnd 8820 findcard2d 9106 ac6sfi 9227 iunfi 9280 elirrv 9528 kmlem2 10083 fin1a2lem10 10341 hsmexlem4 10361 iunfo 10471 modfsummodslem1 15669 lcmfunsnlem2lem1 16506 coprmprod 16529 coprmproddvdslem 16530 lbsextlem4 20607 frlmlbs 21188 coe1fzgsumdlem 21656 evl1gsumdlem 21706 maducoeval2 21973 dishaus 22717 dis2ndc 22795 dislly 22832 dissnlocfin 22864 comppfsc 22867 txdis 22967 txdis1cn 22970 txkgen 22987 isufil2 23243 alexsubALTlem4 23385 tmdgsum 23430 dscopn 23913 ovolfiniun 24849 volfiniun 24895 jensen 26322 uvtx01vtx 28231 cplgr1vlem 28263 unidifsnel 31348 gsumpart 31780 extdg1id 32229 irngss 32238 esum2dlem 32560 bnj1498 33542 funen1cnv 33561 cvmlift2lem1 33765 funpartlem 34494 topdifinffinlem 35785 fvineqsneq 35850 pibt2 35855 finixpnum 36030 mbfresfi 36091 pclfinN 38330 sn-iotalem 40609 mzpcompact2lem 41012 fourierdlem48 44327 sge0sup 44564 funressnvmo 45211 c0snmgmhm 46144 |
Copyright terms: Public domain | W3C validator |