![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > ssexg | Unicode version |
Description: The subset of a set is also a set. Exercise 3 of [TakeutiZaring] p. 22 (generalized). (Contributed by NM, 14-Aug-1994.) |
Ref | Expression |
---|---|
ssexg |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sseq2 3181 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | imbi1d 231 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | vex 2742 |
. . . 4
![]() ![]() ![]() ![]() | |
4 | 3 | ssex 4142 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
5 | 2, 4 | vtoclg 2799 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
6 | 5 | impcom 125 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-io 709 ax-5 1447 ax-7 1448 ax-gen 1449 ax-ie1 1493 ax-ie2 1494 ax-8 1504 ax-10 1505 ax-11 1506 ax-i12 1507 ax-bndl 1509 ax-4 1510 ax-17 1526 ax-i9 1530 ax-ial 1534 ax-i5r 1535 ax-ext 2159 ax-sep 4123 |
This theorem depends on definitions: df-bi 117 df-tru 1356 df-nf 1461 df-sb 1763 df-clab 2164 df-cleq 2170 df-clel 2173 df-nfc 2308 df-v 2741 df-in 3137 df-ss 3144 |
This theorem is referenced by: ssexd 4145 difexg 4146 rabexg 4148 elssabg 4150 elpw2g 4158 abssexg 4184 snexg 4186 sess1 4339 sess2 4340 trsuc 4424 unexb 4444 abnexg 4448 uniexb 4475 xpexg 4742 riinint 4890 dmexg 4893 rnexg 4894 resexg 4949 resiexg 4954 imaexg 4984 exse2 5004 cnvexg 5168 coexg 5175 fabexg 5405 f1oabexg 5475 relrnfvex 5535 fvexg 5536 sefvex 5538 mptfvex 5603 mptexg 5743 ofres 6099 resfunexgALT 6111 cofunexg 6112 fnexALT 6114 f1dmex 6119 oprabexd 6130 mpoexxg 6213 tposexg 6261 frecabex 6401 erex 6561 mapex 6656 pmvalg 6661 elpmg 6666 elmapssres 6675 pmss12g 6677 ixpexgg 6724 ssdomg 6780 fiprc 6817 fival 6971 iccen 10008 shftfvalg 10829 shftfval 10832 tgval 12716 tgvalex 12717 toponsspwpwg 13607 eltg 13637 eltg2 13638 tgss 13648 basgen2 13666 bastop1 13668 topnex 13671 resttopon 13756 restabs 13760 lmfval 13777 cnrest 13820 txss12 13851 metrest 14091 dvbss 14239 dvcnp2cntop 14248 dvaddxxbr 14250 dvmulxxbr 14251 |
Copyright terms: Public domain | W3C validator |