| 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 3484 | . 2 ⊢ 𝑥 ∈ V | |
| 2 | 1 | snid 4662 | 1 ⊢ 𝑥 ∈ {𝑥} |
| Colors of variables: wff setvar class |
| Syntax hints: ∈ wcel 2108 {csn 4626 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-tru 1543 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-v 3482 df-sn 4627 |
| This theorem is referenced by: exsnrex 4680 rext 5453 unipw 5455 xpdifid 6188 opabiota 6991 fnressn 7178 fressnfv 7180 snnex 7778 frrlem12 8322 frrlem14 8324 wfrlem14OLD 8362 wfrlem16OLD 8364 mapsnd 8926 findcard2d 9206 ac6sfi 9320 iunfi 9383 elirrv 9636 kmlem2 10192 fin1a2lem10 10449 hsmexlem4 10469 iunfo 10579 modfsummodslem1 15828 lcmfunsnlem2lem1 16675 coprmprod 16698 coprmproddvdslem 16699 c0snmgmhm 20462 lbsextlem4 21163 frlmlbs 21817 coe1fzgsumdlem 22307 evl1gsumdlem 22360 maducoeval2 22646 dishaus 23390 dis2ndc 23468 dislly 23505 dissnlocfin 23537 comppfsc 23540 txdis 23640 txdis1cn 23643 txkgen 23660 isufil2 23916 alexsubALTlem4 24058 tmdgsum 24103 dscopn 24586 ovolfiniun 25536 volfiniun 25582 jensen 27032 uvtx01vtx 29414 cplgr1vlem 29446 unidifsnel 32553 gsumpart 33060 extdg1id 33716 irngss 33737 esum2dlem 34093 bnj1498 35075 funen1cnv 35102 wevgblacfn 35114 cvmlift2lem1 35307 funpartlem 35943 topdifinffinlem 37348 fvineqsneq 37413 pibt2 37418 finixpnum 37612 mbfresfi 37673 pclfinN 39902 sn-iotalem 42260 mzpcompact2lem 42762 dvmptfprod 45960 fourierdlem48 46169 sge0sup 46406 funressnvmo 47057 dfclnbgr6 47842 dfsclnbgr6 47844 |
| Copyright terms: Public domain | W3C validator |