| 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 5321 | . 2 ⊢ (𝐴 ⊆ 𝐵 → 𝐴 ∈ V) |
| 4 | 1, 3 | ax-mp 5 | 1 ⊢ 𝐴 ∈ V |
| Colors of variables: wff setvar class |
| Syntax hints: ∈ wcel 2108 Vcvv 3480 ⊆ wss 3951 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-ext 2708 ax-sep 5296 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-3an 1089 df-tru 1543 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-rab 3437 df-v 3482 df-in 3958 df-ss 3968 |
| This theorem is referenced by: abex 5326 zfausab 5332 ord3ex 5387 epse 5667 opabex 7240 opabresex2 7485 mptexw 7977 fvclex 7983 oprabex 8001 mpoexw 8103 tfrlem16 8433 fosetex 8898 f1osetex 8899 dffi3 9471 r0weon 10052 dfac3 10161 dfac5lem4 10166 dfac5lem4OLD 10168 dfac2b 10171 hsmexlem6 10471 domtriomlem 10482 axdc3lem 10490 ac6 10520 brdom7disj 10571 brdom6disj 10572 niex 10921 enqex 10962 npex 11026 nrex1 11104 enrex 11107 reex 11246 nnex 12272 zex 12622 qex 13003 ixxex 13398 ltweuz 14002 seqexw 14058 cshwsexa 14862 prmex 16714 prdsval 17500 prdsle 17507 sectfval 17795 sscpwex 17859 issubc 17880 isfunc 17909 fullfunc 17953 fthfunc 17954 isfull 17957 isfth 17961 ipoval 18575 letsr 18638 ressmulgnn 19094 nmznsg 19186 eqgfval 19194 isghm 19233 isghmOLD 19234 lpival 21334 xrsle 21400 znle 21551 cssval 21700 pjfval 21726 ltbval 22061 opsrle 22065 istopon 22918 dmtopon 22929 leordtval2 23220 lecldbas 23227 xkoopn 23597 xkouni 23607 xkoccn 23627 xkoco1cn 23665 xkoco2cn 23666 xkococn 23668 xkoinjcn 23695 uzrest 23905 ustfn 24210 ustn0 24229 isphtpc 25026 tcphex 25251 tchnmfval 25262 bcthlem1 25358 bcthlem5 25362 dyadmbl 25635 itg2seq 25777 aannenlem3 26372 psercn 26470 abelth 26485 vmadivsum 27526 rpvmasumlem 27531 mudivsum 27574 selberglem1 27589 selberglem2 27590 selberg2lem 27594 selberg2 27595 pntrsumo1 27609 selbergr 27612 iscgrg 28520 isismt 28542 ishlg 28610 ishpg 28767 iscgra 28817 isinag 28846 isleag 28855 wksv 29637 sspval 30742 ajfval 30828 shex 31231 chex 31245 hmopex 31894 ressplusf 32948 inftmrel 33187 isinftm 33188 constrsuc 33779 dmvlsiga 34130 measbase 34198 ismeas 34200 isrnmeas 34201 faeval 34247 eulerpartlemmf 34377 eulerpartlemgvv 34378 signsplypnf 34565 signsply0 34566 afsval 34686 kur14lem7 35217 kur14lem9 35219 satfvsuclem1 35364 fmlasuc0 35389 mppsval 35577 dfon2lem7 35790 colinearex 36061 poimirlem4 37631 heibor1lem 37816 rrnval 37834 lsatset 38991 lcvfbr 39021 cmtfvalN 39211 cvrfval 39269 lineset 39740 psubspset 39746 psubclsetN 39938 lautset 40084 pautsetN 40100 tendoset 40761 dicval 41178 ltex 42286 leex 42287 sn-isghm 42683 eldiophb 42768 pellexlem3 42842 pellexlem5 42844 onfrALTlem3VD 44907 modelaxreplem1 44995 rpex 45357 dmvolsal 46361 smfresal 46803 smfliminflem 46845 upwordsseti 46900 amgmlemALT 49322 |
| Copyright terms: Public domain | W3C validator |