Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > ssexg | Structured version Visualization version GIF 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 | ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝐶) → 𝐴 ∈ V) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sseq2 3990 | . . . 4 ⊢ (𝑥 = 𝐵 → (𝐴 ⊆ 𝑥 ↔ 𝐴 ⊆ 𝐵)) | |
2 | 1 | imbi1d 343 | . . 3 ⊢ (𝑥 = 𝐵 → ((𝐴 ⊆ 𝑥 → 𝐴 ∈ V) ↔ (𝐴 ⊆ 𝐵 → 𝐴 ∈ V))) |
3 | vex 3495 | . . . 4 ⊢ 𝑥 ∈ V | |
4 | 3 | ssex 5216 | . . 3 ⊢ (𝐴 ⊆ 𝑥 → 𝐴 ∈ V) |
5 | 2, 4 | vtoclg 3565 | . 2 ⊢ (𝐵 ∈ 𝐶 → (𝐴 ⊆ 𝐵 → 𝐴 ∈ V)) |
6 | 5 | impcom 408 | 1 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝐶) → 𝐴 ∈ V) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 = wceq 1528 ∈ 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: ssexd 5219 prcssprc 5220 difexg 5222 rabexg 5225 elssabg 5230 elpw2g 5238 abssexg 5273 snexALT 5274 sess1 5516 sess2 5517 riinint 5832 resexg 5891 trsuc 6268 ordsssuc2 6272 mptexg 6975 mptexgf 6976 isofr2 7086 ofres 7414 brrpssg 7440 unexb 7460 xpexg 7462 abnexg 7467 difex2 7471 uniexr 7474 dmexg 7602 rnexg 7603 resiexg 7608 imaexg 7609 exse2 7611 cnvexg 7618 coexg 7623 fabexg 7628 f1oabexg 7631 resfunexgALT 7638 cofunexg 7639 fnexALT 7641 f1dmex 7647 oprabexd 7665 mpoexxg 7762 suppfnss 7844 tposexg 7895 tz7.48-3 8069 oaabs 8260 erex 8302 mapex 8401 pmvalg 8406 elpmg 8411 elmapssres 8420 pmss12g 8422 ralxpmap 8448 ixpexg 8474 ssdomg 8543 fiprc 8583 domunsncan 8605 infensuc 8683 pssnn 8724 unbnn 8762 fodomfi 8785 fival 8864 fiss 8876 dffi3 8883 hartogslem2 8995 card2on 9006 wdomima2g 9038 unxpwdom2 9040 unxpwdom 9041 harwdom 9042 oemapvali 9135 ackbij1lem11 9640 cofsmo 9679 ssfin4 9720 fin23lem11 9727 ssfin2 9730 ssfin3ds 9740 isfin1-3 9796 hsmex3 9844 axdc2lem 9858 ac6num 9889 ttukeylem1 9919 dmct 9934 ondomon 9973 fpwwe2lem3 10043 fpwwe2lem12 10051 fpwwe2lem13 10052 canthwe 10061 wuncss 10155 genpv 10409 genpdm 10412 hashss 13758 hashf1lem1 13801 wrdexgOLD 13860 wrdexb 13861 shftfval 14417 o1of2 14957 o1rlimmul 14963 isercolllem2 15010 isstruct2 16481 ressval3d 16549 ressabs 16551 prdsbas 16718 fnmrc 16866 mrcfval 16867 isacs1i 16916 mreacs 16917 isssc 17078 ipolerval 17754 ress0g 17927 symgbas 18436 sylow2a 18673 islbs3 19856 toponsspwpw 21458 basdif0 21489 tgval 21491 eltg 21493 eltg2 21494 tgss 21504 basgen2 21525 2basgen 21526 bastop1 21529 topnex 21532 resttopon 21697 restabs 21701 restcld 21708 restfpw 21715 restcls 21717 restntr 21718 ordtbas2 21727 ordtbas 21728 lmfval 21768 cnrest 21821 cmpcov 21925 cmpsublem 21935 cmpsub 21936 2ndcomap 21994 islocfin 22053 txss12 22141 ptrescn 22175 trfbas2 22379 trfbas 22380 isfildlem 22393 snfbas 22402 trfil1 22422 trfil2 22423 trufil 22446 ssufl 22454 hauspwpwf1 22523 ustval 22738 metrest 23061 cnheibor 23486 metcld2 23837 bcthlem1 23854 mbfimaopn2 24185 0pledm 24201 dvbss 24426 dvreslem 24434 dvres2lem 24435 dvcnp2 24444 dvaddbr 24462 dvmulbr 24463 dvcnvrelem2 24542 elply2 24713 plyf 24715 plyss 24716 elplyr 24718 plyeq0lem 24727 plyeq0 24728 plyaddlem 24732 plymullem 24733 dgrlem 24746 coeidlem 24754 ulmcn 24914 pserulm 24937 rabexgfGS 30189 abrexdomjm 30194 aciunf1 30336 ress1r 30787 pcmplfin 31023 metidval 31029 indval 31171 sigagenss 31307 measval 31356 omsfval 31451 omssubaddlem 31456 omssubadd 31457 carsggect 31475 erdsze2lem1 32347 erdsze2lem2 32348 cvxpconn 32386 elmsta 32692 dfon2lem3 32927 altxpexg 33336 ivthALT 33580 filnetlem3 33625 bj-elpwg 34239 bj-restsnss 34268 bj-restsnss2 34269 bj-restb 34279 bj-restuni2 34283 abrexdom 34886 sdclem2 34898 sdclem1 34899 imaexALTV 35468 brssr 35621 pssexg 38990 elrfirn 39170 pwssplit4 39567 hbtlem1 39601 hbtlem7 39603 inaex 40510 rabexgf 41158 disjinfi 41330 dvnprodlem1 42107 dvnprodlem2 42108 qndenserrnbllem 42456 sge0ss 42571 psmeasurelem 42629 caragensplit 42659 omeunile 42664 caragenuncl 42672 omeunle 42675 omeiunlempt 42679 carageniuncllem2 42681 frnvafv2v 43312 prprval 43553 mpoexxg2 44314 gsumlsscl 44359 lincellss 44409 |
Copyright terms: Public domain | W3C validator |