![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > ssexg | Structured version Visualization version 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 3466 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | imbi1d 323 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | vex 3060 |
. . . 4
![]() ![]() ![]() ![]() | |
4 | 3 | ssex 4561 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
5 | 2, 4 | vtoclg 3119 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
6 | 5 | impcom 436 |
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 1680 ax-4 1693 ax-5 1769 ax-6 1816 ax-7 1862 ax-10 1926 ax-11 1931 ax-12 1944 ax-13 2102 ax-ext 2442 ax-sep 4539 |
This theorem depends on definitions: df-bi 190 df-an 377 df-tru 1458 df-ex 1675 df-nf 1679 df-sb 1809 df-clab 2449 df-cleq 2455 df-clel 2458 df-nfc 2592 df-v 3059 df-in 3423 df-ss 3430 |
This theorem is referenced by: ssexd 4564 difexg 4565 rabexg 4567 elssabg 4572 elpw2g 4580 abssexg 4602 snexALT 4603 sess1 4821 sess2 4822 riinint 5110 resexg 5166 trsuc 5526 ordsssuc2 5530 mptexg 6160 isofr2 6260 ofres 6574 brrpssg 6600 unexb 6618 xpexg 6620 difex2 6625 uniexb 6628 dmexg 6751 rnexg 6752 resiexg 6756 imaexg 6757 exse2 6759 cnvexg 6766 coexg 6771 fabexg 6776 f1oabexg 6779 resfunexgALT 6783 cofunexg 6784 fnexALT 6786 f1dmex 6790 oprabexd 6807 mpt2exxg 6894 suppfnss 6967 tposexg 7013 tz7.48-3 7187 oaabs 7371 erex 7413 mapex 7504 pmvalg 7509 elpmg 7513 elmapssres 7522 pmss12g 7524 ralxpmap 7547 ixpexg 7572 ssdomg 7641 fiprc 7677 domunsncan 7698 infensuc 7776 pssnn 7816 unbnn 7853 fodomfi 7876 fival 7952 fiss 7964 dffi3 7971 hartogslem2 8084 card2on 8095 wdomima2g 8127 unxpwdom2 8129 unxpwdom 8130 harwdom 8131 oemapvali 8215 ackbij1lem11 8686 cofsmo 8725 ssfin4 8766 fin23lem11 8773 ssfin2 8776 ssfin3ds 8786 isfin1-3 8842 hsmex3 8890 axdc2lem 8904 ac6num 8935 ttukeylem1 8965 ondomon 9014 fpwwe2lem3 9084 fpwwe2lem12 9092 fpwwe2lem13 9093 canthwe 9102 wuncss 9196 genpv 9450 genpdm 9453 hashss 12618 hashf1lem1 12651 wrdexg 12715 wrdexb 12716 shftfval 13182 o1of2 13725 o1rlimmul 13731 isercolllem2 13778 isstruct2 15179 ressval3d 15235 ressabs 15237 prdsbas 15404 fnmrc 15562 mrcfval 15563 isacs1i 15612 mreacs 15613 isssc 15774 ipolerval 16451 ress0g 16614 symgbas 17070 sylow2a 17320 islbs3 18427 basdif0 20017 tgval 20019 eltg 20021 eltg2 20022 tgss 20033 basgen2 20054 2basgen 20055 bastop1 20058 resttopon 20226 restabs 20230 restcld 20237 restfpw 20244 restcls 20246 restntr 20247 ordtbas2 20256 ordtbas 20257 lmfval 20297 cnrest 20350 cmpcov 20453 cmpsublem 20463 cmpsub 20464 2ndcomap 20522 islocfin 20581 txss12 20669 ptrescn 20703 trfbas2 20907 trfbas 20908 isfildlem 20921 snfbas 20930 trfil1 20950 trfil2 20951 trufil 20974 ssufl 20982 hauspwpwf1 21051 ustval 21266 metrest 21588 cnheibor 22032 metcld2 22325 bcthlem1 22341 mbfimaopn2 22662 0pledm 22680 dvbss 22905 dvreslem 22913 dvres2lem 22914 dvcnp2 22923 dvaddbr 22941 dvmulbr 22942 dvcnvrelem2 23019 elply2 23199 plyf 23201 plyss 23202 elplyr 23204 plyeq0lem 23213 plyeq0 23214 plyaddlem 23218 plymullem 23219 dgrlem 23232 coeidlem 23240 ulmcn 23403 pserulm 23426 iseupa 25742 issubgo 26080 rabexgfGS 28186 abrexdomjm 28190 mptexgf 28274 aciunf1 28314 dmct 28347 ress1r 28601 pcmplfin 28736 metidval 28742 indval 28884 sigagenss 29020 measval 29069 omsfval 29167 omsfvalOLD 29171 omssubaddlem 29176 omssubadd 29177 omssubaddlemOLD 29180 omssubaddOLD 29181 elcarsg 29186 carsggect 29199 carsgclctunlem3 29201 erdsze2lem1 29975 erdsze2lem2 29976 cvxpcon 30014 elmsta 30235 dfon2lem3 30480 altxpexg 30794 ivthALT 31040 filnetlem3 31085 abrexdom 32102 sdclem2 32116 sdclem1 32117 elrfirn 35582 pwssplit4 35992 hbtlem1 36027 hbtlem7 36029 rabexgf 37385 wessf1ornlem 37497 disjinfi 37506 dvnprodlem1 37859 dvnprodlem2 37860 qndenserrnbllem 38201 sge0ss 38292 psmeasurelem 38346 caragensplit 38359 omeunile 38364 caragenuncl 38372 omeunle 38375 omeiunlempt 38379 carageniuncllem2 38381 prcssprc 39024 mpt2exxg2 40392 gsumlsscl 40441 lincellss 40492 |
Copyright terms: Public domain | W3C validator |