Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > snid | Unicode version |
Description: A set is a member of its singleton. Part of Theorem 7.6 of [Quine] p. 49. (Contributed by NM, 31-Dec-1993.) |
Ref | Expression |
---|---|
snid.1 |
Ref | Expression |
---|---|
snid |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | snid.1 | . 2 | |
2 | snidb 3600 | . 2 | |
3 | 1, 2 | mpbi 144 | 1 |
Colors of variables: wff set class |
Syntax hints: wcel 2135 cvv 2721 csn 3570 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-io 699 ax-5 1434 ax-7 1435 ax-gen 1436 ax-ie1 1480 ax-ie2 1481 ax-8 1491 ax-10 1492 ax-11 1493 ax-i12 1494 ax-bndl 1496 ax-4 1497 ax-17 1513 ax-i9 1517 ax-ial 1521 ax-i5r 1522 ax-ext 2146 |
This theorem depends on definitions: df-bi 116 df-tru 1345 df-nf 1448 df-sb 1750 df-clab 2151 df-cleq 2157 df-clel 2160 df-nfc 2295 df-v 2723 df-sn 3576 |
This theorem is referenced by: vsnid 3602 exsnrex 3612 rabsnt 3645 sneqr 3734 undifexmid 4166 exmidexmid 4169 ss1o0el1 4170 exmidundif 4179 exmidundifim 4180 unipw 4189 intid 4196 ordtriexmidlem2 4491 ordtriexmid 4492 ontriexmidim 4493 ordtri2orexmid 4494 regexmidlem1 4504 0elsucexmid 4536 ordpwsucexmid 4541 opthprc 4649 fsn 5651 fsn2 5653 fvsn 5674 fvsnun1 5676 acexmidlema 5827 acexmidlemb 5828 acexmidlemab 5830 brtpos0 6211 mapsn 6647 mapsncnv 6652 0elixp 6686 en1 6756 djulclr 7005 djurclr 7006 djulcl 7007 djurcl 7008 djuf1olem 7009 exmidonfinlem 7140 elreal2 7762 1exp 10474 hashinfuni 10679 ennnfonelemhom 12291 dvef 13235 djucllem 13522 bj-d0clsepcl 13648 exmid1stab 13721 |
Copyright terms: Public domain | W3C validator |