Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > ssexi | Structured version Visualization version GIF version |
Description: The subset of a set is also a set. (Contributed by NM, 9-Sep-1993.) |
Ref | Expression |
---|---|
ssexi.1 | ⊢ 𝐵 ∈ V |
ssexi.2 | ⊢ 𝐴 ⊆ 𝐵 |
Ref | Expression |
---|---|
ssexi | ⊢ 𝐴 ∈ V |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ssexi.2 | . 2 ⊢ 𝐴 ⊆ 𝐵 | |
2 | ssexi.1 | . . 3 ⊢ 𝐵 ∈ V | |
3 | 2 | ssex 5216 | . 2 ⊢ (𝐴 ⊆ 𝐵 → 𝐴 ∈ V) |
4 | 1, 3 | ax-mp 5 | 1 ⊢ 𝐴 ∈ V |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2105 Vcvv 3492 ⊆ wss 3933 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-8 2107 ax-9 2115 ax-10 2136 ax-11 2151 ax-12 2167 ax-ext 2790 ax-sep 5194 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 842 df-tru 1531 df-ex 1772 df-nf 1776 df-sb 2061 df-clab 2797 df-cleq 2811 df-clel 2890 df-nfc 2960 df-rab 3144 df-v 3494 df-in 3940 df-ss 3949 |
This theorem is referenced by: zfausab 5224 ord3ex 5278 epse 5531 opabex 6974 mptexw 7643 fvclex 7649 oprabex 7666 mpoexw 7765 tfrlem16 8018 dffi3 8883 r0weon 9426 dfac3 9535 dfac5lem4 9540 dfac2b 9544 hsmexlem6 9841 domtriomlem 9852 axdc3lem 9860 ac6 9890 brdom7disj 9941 brdom6disj 9942 niex 10291 enqex 10332 npex 10396 nrex1 10474 enrex 10477 reex 10616 nnex 11632 zex 11978 qex 12348 ixxex 12737 ltweuz 13317 seqexw 13373 prmex 16009 prdsval 16716 prdsle 16723 sectfval 17009 sscpwex 17073 issubc 17093 isfunc 17122 fullfunc 17164 fthfunc 17165 isfull 17168 isfth 17172 ipoval 17752 letsr 17825 nmznsg 18258 eqgfval 18266 isghm 18296 symgval 18435 lpival 19946 ltbval 20180 opsrle 20184 xrsle 20493 znle 20611 cssval 20754 pjfval 20778 istopon 21448 dmtopon 21459 leordtval2 21748 lecldbas 21755 xkoopn 22125 xkouni 22135 xkoccn 22155 xkoco1cn 22193 xkoco2cn 22194 xkococn 22196 xkoinjcn 22223 uzrest 22433 ustfn 22737 ustn0 22756 isphtpc 23525 tcphex 23747 tchnmfval 23758 bcthlem1 23854 bcthlem5 23858 dyadmbl 24128 itg2seq 24270 aannenlem3 24846 psercn 24941 abelth 24956 vmadivsum 25985 rpvmasumlem 25990 mudivsum 26033 selberglem1 26048 selberglem2 26049 selberg2lem 26053 selberg2 26054 pntrsumo1 26068 selbergr 26071 iscgrg 26225 isismt 26247 ishlg 26315 ishpg 26472 iscgra 26522 isinag 26551 isleag 26560 pthsfval 27429 spthsfval 27430 crcts 27496 cycls 27497 eupths 27906 sspval 28427 ajfval 28513 shex 28916 chex 28930 hmopex 29579 ressplusf 30564 ressmulgnn 30597 inftmrel 30736 isinftm 30737 dmvlsiga 31287 measbase 31355 ismeas 31357 isrnmeas 31358 faeval 31404 eulerpartlemmf 31532 eulerpartlemgvv 31533 signsplypnf 31719 signsply0 31720 afsval 31841 kur14lem7 32356 kur14lem9 32358 satfvsuclem1 32503 fmlasuc0 32528 mppsval 32716 dfon2lem7 32931 colinearex 33418 poimirlem4 34777 heibor1lem 34968 rrnval 34986 lsatset 36006 lcvfbr 36036 cmtfvalN 36226 cvrfval 36284 lineset 36754 psubspset 36760 psubclsetN 36952 lautset 37098 pautsetN 37114 tendoset 37775 dicval 38192 eldiophb 39232 pellexlem3 39306 pellexlem5 39308 onfrALTlem3VD 41098 dmvolsal 42506 smfresal 42940 smfliminflem 42981 amgmlemALT 44832 |
Copyright terms: Public domain | W3C validator |