![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
Mirrors > Home > MPE Home > Th. List > snssi | Unicode version |
Description: The singleton of an element of a class is a subset of the class. (Contributed by NM, 6-Jun-1994.) |
Ref | Expression |
---|---|
snssi |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | snssg 3892 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | ibi 233 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() ![]() |
This theorem is referenced by: difsnid 3904 pwpw0 3906 sssn 3917 ssunsn2 3918 tpssi 3925 pwsnALT 3970 snelpwi 4369 intid 4381 suceloni 4752 xpsspw 4945 xpsspwOLD 4946 djussxp 4977 xpimasn 5275 fconst6g 5591 dffv2 5755 fvimacnvi 5803 fvimacnvALT 5808 fsn2 5867 fsnunf 5890 curry1 6397 curry2 6400 mapsn 7014 fodomr 7217 sucdom2 7262 en1eqsn 7297 enp1ilem 7301 findcard2 7307 findcard2s 7308 marypha1lem 7396 marypha2lem1 7398 epfrs 7623 dfac5lem4 7963 kmlem11 7996 ackbij1lem2 8057 fin23lem26 8161 isfin1-3 8222 hsmexlem4 8265 axdc3lem4 8289 axresscn 8979 nn0ssre 10181 xrsupss 10843 supxrmnf 10852 1fv 11075 1exp 11364 hashxrcl 11595 hashdifsn 11634 brfi1indlem 11669 s1cl 11710 fsum00 12532 incexc 12572 xpnnenOLD 12764 2ebits 12914 bitsinvp1 12916 4sqlem19 13286 ramxrcl 13340 strlemor1 13511 mrcsncl 13792 acsfn1 13841 homaf 14140 dmcoass 14176 lubel 14504 gsumws1 14740 cycsubg2 14932 cntzsnval 15078 0frgp 15366 dpjidcl 15571 ablfac1eu 15586 lspsncl 16008 lspsnss 16021 lspsnid 16024 lpival 16271 lpiss 16276 lidldvgen 16281 znlidl 16769 frgpcyg 16809 isneip 17124 neips 17132 opnneip 17138 maxlp 17165 restsn2 17189 leordtval2 17230 ist1-3 17367 ordtt1 17397 2ndcdisj2 17473 uffix 17906 neiflim 17959 ptcmplem5 18040 cnextfres 18052 haustsms2 18119 ust0 18202 ustuqtop5 18228 dscopn 18574 icccmplem1 18806 bndth 18936 ovolsn 19344 icombl1 19410 plyun0 20069 coeeulem 20096 coeeu 20097 vieta1lem2 20181 aalioulem2 20203 taylfval 20228 perfectlem2 20967 konigsberg 21662 hsn0elch 22703 chsupsn 22868 chsup0 23003 h1deoi 23004 h1dei 23005 h1did 23006 h1de2ctlem 23010 h1de2ci 23011 spansni 23012 spansnch 23015 elspansncl 23020 spansnpji 23033 spanunsni 23034 spanpr 23035 h1datomi 23036 spansnji 23101 h1da 23805 atom1d 23809 superpos 23810 esumnul 24396 esumcst 24408 hashf2 24427 measvuni 24521 cntnevol 24535 ballotlemfp1 24702 dfon2lem3 25355 altxpsspw 25726 axlowdimlem7 25791 axlowdimlem10 25794 mblfinlem 26143 dvreasin 26179 fdc 26339 prnc 26567 isfldidl 26568 ispridlc 26570 ralxpmap 26632 mapfzcons 26662 mzpcompact2lem 26698 diophrw 26707 frlmlbs 27117 stoweidlem44 27660 dmressnsn 27852 fnbrafvb 27885 afvres 27903 snelpwrVD 28652 islshpsm 29463 snatpsubN 30232 polatN 30413 atpsubclN 30427 pclfinclN 30432 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-3 7 ax-mp 8 ax-gen 1552 ax-5 1563 ax-17 1623 ax-9 1662 ax-8 1683 ax-6 1740 ax-7 1745 ax-11 1757 ax-12 1946 ax-ext 2385 |
This theorem depends on definitions: df-bi 178 df-an 361 df-tru 1325 df-ex 1548 df-nf 1551 df-sb 1656 df-clab 2391 df-cleq 2397 df-clel 2400 df-nfc 2529 df-v 2918 df-in 3287 df-ss 3294 df-sn 3780 |
Copyright terms: Public domain | W3C validator |