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 3121 | . . . 4 | |
2 | 1 | imbi1d 230 | . . 3 |
3 | vex 2689 | . . . 4 | |
4 | 3 | ssex 4065 | . . 3 |
5 | 2, 4 | vtoclg 2746 | . 2 |
6 | 5 | impcom 124 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wa 103 wceq 1331 wcel 1480 cvv 2686 wss 3071 |
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 698 ax-5 1423 ax-7 1424 ax-gen 1425 ax-ie1 1469 ax-ie2 1470 ax-8 1482 ax-10 1483 ax-11 1484 ax-i12 1485 ax-bndl 1486 ax-4 1487 ax-17 1506 ax-i9 1510 ax-ial 1514 ax-i5r 1515 ax-ext 2121 ax-sep 4046 |
This theorem depends on definitions: df-bi 116 df-tru 1334 df-nf 1437 df-sb 1736 df-clab 2126 df-cleq 2132 df-clel 2135 df-nfc 2270 df-v 2688 df-in 3077 df-ss 3084 |
This theorem is referenced by: ssexd 4068 difexg 4069 rabexg 4071 elssabg 4073 elpw2g 4081 abssexg 4106 snexg 4108 sess1 4259 sess2 4260 trsuc 4344 unexb 4363 abnexg 4367 uniexb 4394 xpexg 4653 riinint 4800 dmexg 4803 rnexg 4804 resexg 4859 resiexg 4864 imaexg 4893 exse2 4913 cnvexg 5076 coexg 5083 fabexg 5310 f1oabexg 5379 relrnfvex 5439 fvexg 5440 sefvex 5442 mptfvex 5506 mptexg 5645 ofres 5996 resfunexgALT 6008 cofunexg 6009 fnexALT 6011 f1dmex 6014 oprabexd 6025 mpoexxg 6108 tposexg 6155 frecabex 6295 erex 6453 mapex 6548 pmvalg 6553 elpmg 6558 elmapssres 6567 pmss12g 6569 ixpexgg 6616 ssdomg 6672 fiprc 6709 fival 6858 shftfvalg 10590 shftfval 10593 toponsspwpwg 12189 tgval 12218 tgvalex 12219 eltg 12221 eltg2 12222 tgss 12232 basgen2 12250 bastop1 12252 topnex 12255 resttopon 12340 restabs 12344 lmfval 12361 cnrest 12404 txss12 12435 metrest 12675 dvbss 12823 dvcnp2cntop 12832 dvaddxxbr 12834 dvmulxxbr 12835 |
Copyright terms: Public domain | W3C validator |