![]() |
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 5320 | . 2 ⊢ (𝐴 ⊆ 𝐵 → 𝐴 ∈ V) |
4 | 1, 3 | ax-mp 5 | 1 ⊢ 𝐴 ∈ V |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2106 Vcvv 3474 ⊆ wss 3947 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-ext 2703 ax-sep 5298 |
This theorem depends on definitions: df-bi 206 df-an 397 df-tru 1544 df-ex 1782 df-sb 2068 df-clab 2710 df-cleq 2724 df-clel 2810 df-rab 3433 df-v 3476 df-in 3954 df-ss 3964 |
This theorem is referenced by: zfausab 5329 ord3ex 5384 epse 5658 opabex 7218 opabresex2 7457 mptexw 7935 fvclex 7941 oprabex 7959 mpoexw 8061 tfrlem16 8389 fosetex 8848 f1osetex 8849 dffi3 9422 r0weon 10003 dfac3 10112 dfac5lem4 10117 dfac2b 10121 hsmexlem6 10422 domtriomlem 10433 axdc3lem 10441 ac6 10471 brdom7disj 10522 brdom6disj 10523 niex 10872 enqex 10913 npex 10977 nrex1 11055 enrex 11058 reex 11197 nnex 12214 zex 12563 qex 12941 ixxex 13331 ltweuz 13922 seqexw 13978 cshwsexa 14770 prmex 16610 prdsval 17397 prdsle 17404 sectfval 17694 sscpwex 17758 issubc 17781 isfunc 17810 fullfunc 17853 fthfunc 17854 isfull 17857 isfth 17861 ipoval 18479 letsr 18542 nmznsg 19042 eqgfval 19050 isghm 19086 lpival 20875 xrsle 20957 znle 21079 cssval 21226 pjfval 21252 ltbval 21589 opsrle 21593 istopon 22405 dmtopon 22416 leordtval2 22707 lecldbas 22714 xkoopn 23084 xkouni 23094 xkoccn 23114 xkoco1cn 23152 xkoco2cn 23153 xkococn 23155 xkoinjcn 23182 uzrest 23392 ustfn 23697 ustn0 23716 isphtpc 24501 tcphex 24725 tchnmfval 24736 bcthlem1 24832 bcthlem5 24836 dyadmbl 25108 itg2seq 25251 aannenlem3 25834 psercn 25929 abelth 25944 vmadivsum 26974 rpvmasumlem 26979 mudivsum 27022 selberglem1 27037 selberglem2 27038 selberg2lem 27042 selberg2 27043 pntrsumo1 27057 selbergr 27060 iscgrg 27752 isismt 27774 ishlg 27842 ishpg 27999 iscgra 28049 isinag 28078 isleag 28087 wksv 28865 sspval 29963 ajfval 30049 shex 30452 chex 30466 hmopex 31115 ressplusf 32114 ressmulgnn 32171 inftmrel 32313 isinftm 32314 dmvlsiga 33115 measbase 33183 ismeas 33185 isrnmeas 33186 faeval 33232 eulerpartlemmf 33362 eulerpartlemgvv 33363 signsplypnf 33549 signsply0 33550 afsval 33671 kur14lem7 34191 kur14lem9 34193 satfvsuclem1 34338 fmlasuc0 34363 mppsval 34551 dfon2lem7 34749 colinearex 35020 poimirlem4 36480 heibor1lem 36665 rrnval 36683 lsatset 37848 lcvfbr 37878 cmtfvalN 38068 cvrfval 38126 lineset 38597 psubspset 38603 psubclsetN 38795 lautset 38941 pautsetN 38957 tendoset 39618 dicval 40035 eldiophb 41480 pellexlem3 41554 pellexlem5 41556 onfrALTlem3VD 43633 dmvolsal 45048 smfresal 45490 smfliminflem 45532 upwordsseti 45585 amgmlemALT 47803 |
Copyright terms: Public domain | W3C validator |