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 3913 | . . . 4 ⊢ (𝑥 = 𝐵 → (𝐴 ⊆ 𝑥 ↔ 𝐴 ⊆ 𝐵)) | |
2 | 1 | imbi1d 345 | . . 3 ⊢ (𝑥 = 𝐵 → ((𝐴 ⊆ 𝑥 → 𝐴 ∈ V) ↔ (𝐴 ⊆ 𝐵 → 𝐴 ∈ V))) |
3 | vex 3402 | . . . 4 ⊢ 𝑥 ∈ V | |
4 | 3 | ssex 5199 | . . 3 ⊢ (𝐴 ⊆ 𝑥 → 𝐴 ∈ V) |
5 | 2, 4 | vtoclg 3471 | . 2 ⊢ (𝐵 ∈ 𝐶 → (𝐴 ⊆ 𝐵 → 𝐴 ∈ V)) |
6 | 5 | impcom 411 | 1 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝐶) → 𝐴 ∈ V) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 399 = wceq 1543 ∈ wcel 2112 Vcvv 3398 ⊆ wss 3853 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 ax-6 1976 ax-7 2018 ax-8 2114 ax-9 2122 ax-ext 2708 ax-sep 5177 |
This theorem depends on definitions: df-bi 210 df-an 400 df-tru 1546 df-ex 1788 df-sb 2073 df-clab 2715 df-cleq 2728 df-clel 2809 df-rab 3060 df-v 3400 df-in 3860 df-ss 3870 |
This theorem is referenced by: ssexd 5202 prcssprc 5203 difexg 5205 rabexg 5209 elssabg 5214 elpw2g 5222 abssexg 5260 snexALT 5261 sess1 5504 sess2 5505 riinint 5822 resexg 5882 trsuc 6275 ordsssuc2 6279 mptexg 7015 mptexgf 7016 isofr2 7131 ofres 7465 brrpssg 7491 unexb 7511 xpexg 7513 abnexg 7519 difex2 7523 uniexr 7526 dmexg 7659 rnexg 7660 resiexg 7670 imaexg 7671 exse2 7673 cnvexg 7680 coexg 7685 fabexg 7690 f1oabexg 7692 resfunexgALT 7699 cofunexg 7700 fnexALT 7702 f1dmex 7708 oprabexd 7726 mpoexxg 7824 suppfnss 7909 tposexg 7960 tz7.48-3 8158 oaabs 8351 erex 8393 mapex 8492 pmvalg 8497 elpmg 8502 elmapssres 8526 pmss12g 8528 ralxpmap 8555 ixpexg 8581 ssdomg 8652 fiprc 8700 domunsncan 8723 infensuc 8802 pssnn 8824 ssfi 8829 pssnnOLD 8872 unbnn 8905 fodomfi 8927 fival 9006 fiss 9018 dffi3 9025 hartogslem2 9137 card2on 9148 wdomima2g 9180 unxpwdom2 9182 unxpwdom 9183 harwdom 9185 oemapvali 9277 ackbij1lem11 9809 cofsmo 9848 ssfin4 9889 fin23lem11 9896 ssfin2 9899 ssfin3ds 9909 isfin1-3 9965 hsmex3 10013 axdc2lem 10027 ac6num 10058 ttukeylem1 10088 dmct 10103 ondomon 10142 fpwwe2lem3 10212 fpwwe2lem11 10220 fpwwe2lem12 10221 canthwe 10230 wuncss 10324 genpv 10578 genpdm 10581 hashss 13941 hashf1lem1OLD 13986 wrdexb 14045 shftfval 14598 o1of2 15139 o1rlimmul 15145 isercolllem2 15194 isstruct2 16676 ressval3d 16745 ressabs 16747 prdsbas 16916 fnmrc 17064 mrcfval 17065 isacs1i 17114 mreacs 17115 isssc 17279 ipolerval 17992 ress0g 18155 sylow2a 18962 islbs3 20146 toponsspwpw 21773 basdif0 21804 tgval 21806 eltg 21808 eltg2 21809 tgss 21819 basgen2 21840 2basgen 21841 bastop1 21844 topnex 21847 resttopon 22012 restabs 22016 restcld 22023 restfpw 22030 restcls 22032 restntr 22033 ordtbas2 22042 ordtbas 22043 lmfval 22083 cnrest 22136 cmpcov 22240 cmpsublem 22250 cmpsub 22251 2ndcomap 22309 islocfin 22368 txss12 22456 ptrescn 22490 trfbas2 22694 trfbas 22695 isfildlem 22708 snfbas 22717 trfil1 22737 trfil2 22738 trufil 22761 ssufl 22769 hauspwpwf1 22838 ustval 23054 metrest 23376 cnheibor 23806 metcld2 24158 bcthlem1 24175 mbfimaopn2 24508 0pledm 24524 dvbss 24752 dvreslem 24760 dvres2lem 24761 dvcnp2 24771 dvaddbr 24789 dvmulbr 24790 dvcnvrelem2 24869 elply2 25044 plyf 25046 plyss 25047 elplyr 25049 plyeq0lem 25058 plyeq0 25059 plyaddlem 25063 plymullem 25064 dgrlem 25077 coeidlem 25085 ulmcn 25245 pserulm 25268 rabexgfGS 30519 abrexdomjm 30525 aciunf1 30674 ress1r 31159 pcmplfin 31478 metidval 31508 indval 31647 sigagenss 31783 measval 31832 omsfval 31927 omssubaddlem 31932 omssubadd 31933 carsggect 31951 erdsze2lem1 32832 erdsze2lem2 32833 cvxpconn 32871 elmsta 33177 dfon2lem3 33431 altxpexg 33966 ivthALT 34210 filnetlem3 34255 bj-sselpwuni 34909 bj-elpwg 34911 bj-restsnss 34938 bj-restsnss2 34939 bj-restb 34949 bj-restuni2 34953 abrexdom 35574 sdclem2 35586 sdclem1 35587 imaexALTV 36151 brssr 36305 sticksstones4 39774 sticksstones14 39785 pssexg 39855 elrfirn 40161 pwssplit4 40558 hbtlem1 40592 hbtlem7 40594 inaex 41529 rabexgf 42181 dvnprodlem1 43105 dvnprodlem2 43106 qndenserrnbllem 43453 sge0ss 43568 psmeasurelem 43626 caragensplit 43656 omeunile 43661 caragenuncl 43669 omeunle 43672 omeiunlempt 43676 carageniuncllem2 43678 frnvafv2v 44343 prprval 44582 mpoexxg2 45289 gsumlsscl 45335 lincellss 45383 |
Copyright terms: Public domain | W3C validator |