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 3495 | . 2 ⊢ 𝑥 ∈ V | |
2 | 1 | snid 4591 | 1 ⊢ 𝑥 ∈ {𝑥} |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2105 {csn 4557 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-8 2107 ax-9 2115 ax-10 2136 ax-11 2151 ax-12 2167 ax-ext 2790 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 842 df-tru 1531 df-ex 1772 df-nf 1776 df-sb 2061 df-clab 2797 df-cleq 2811 df-clel 2890 df-nfc 2960 df-v 3494 df-sn 4558 |
This theorem is referenced by: exsnrex 4610 rext 5331 unipw 5333 xpdifid 6018 opabiota 6739 fnressn 6912 fressnfv 6914 snnex 7469 wfrlem14 7957 wfrlem16 7959 mapsnd 8438 findcard2d 8748 ac6sfi 8750 iunfi 8800 elirrv 9048 kmlem2 9565 fin1a2lem10 9819 hsmexlem4 9839 iunfo 9949 modfsummodslem1 15135 lcmfunsnlem2lem1 15970 coprmprod 15993 coprmproddvdslem 15994 lbsextlem4 19862 coe1fzgsumdlem 20397 evl1gsumdlem 20447 frlmlbs 20869 maducoeval2 21177 dishaus 21918 dis2ndc 21996 dislly 22033 dissnlocfin 22065 comppfsc 22068 txdis 22168 txdis1cn 22171 txkgen 22188 isufil2 22444 alexsubALTlem4 22586 tmdgsum 22631 dscopn 23110 ovolfiniun 24029 volfiniun 24075 jensen 25493 uvtx01vtx 27106 cplgr1vlem 27138 unidifsnel 30222 extdg1id 30952 esum2dlem 31250 bnj1498 32230 funen1cnv 32254 cvmlift2lem1 32446 frrlem12 33031 frrlem14 33033 funpartlem 33300 topdifinffinlem 34510 fvineqsneq 34575 pibt2 34580 finixpnum 34758 mbfresfi 34819 pclfinN 36916 mzpcompact2lem 39226 fourierdlem48 42316 sge0sup 42550 funressnvmo 43157 c0snmgmhm 44113 |
Copyright terms: Public domain | W3C validator |