![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > snssg | Structured version Visualization version Unicode version |
Description: The singleton of an element of a class is a subset of the class. Theorem 7.4 of [Quine] p. 49. (Contributed by NM, 22-Jul-2001.) |
Ref | Expression |
---|---|
snssg |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eleq1 2517 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | sneq 3978 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 2 | sseq1d 3459 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | vex 3048 |
. . 3
![]() ![]() ![]() ![]() | |
5 | 4 | snss 4096 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
6 | 1, 3, 5 | vtoclbg 3108 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1669 ax-4 1682 ax-5 1758 ax-6 1805 ax-7 1851 ax-10 1915 ax-11 1920 ax-12 1933 ax-13 2091 ax-ext 2431 |
This theorem depends on definitions: df-bi 189 df-an 373 df-3an 987 df-tru 1447 df-ex 1664 df-nf 1668 df-sb 1798 df-clab 2438 df-cleq 2444 df-clel 2447 df-v 3047 df-in 3411 df-ss 3418 df-sn 3969 |
This theorem is referenced by: tppreqb 4113 snssi 4116 snssd 4117 prssg 4127 fvimacnvALT 6001 fr3nr 6606 vdwapid1 14925 acsfn 15565 cycsubg2 16854 cycsubg2cl 16855 pgpfac1lem1 17707 pgpfac1lem3a 17709 pgpfac1lem3 17710 pgpfac1lem5 17712 pgpfaclem2 17715 lspsnid 18216 lidldvgen 18479 isneip 20121 elnei 20127 iscnp4 20279 cnpnei 20280 nlly2i 20491 1stckgenlem 20568 flimopn 20990 flimclslem 20999 fclsneii 21032 fcfnei 21050 limcvallem 22826 ellimc2 22832 limcflf 22836 limccnp 22846 limccnp2 22847 limcco 22848 lhop2 22967 plyrem 23258 isppw 24041 h1did 27204 erdszelem8 29921 neibastop2 31017 prnc 32300 proot1mul 36073 islptre 37699 |
Copyright terms: Public domain | W3C validator |