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 3952 | . . . 4 ⊢ (𝑥 = 𝐵 → (𝐴 ⊆ 𝑥 ↔ 𝐴 ⊆ 𝐵)) | |
2 | 1 | imbi1d 342 | . . 3 ⊢ (𝑥 = 𝐵 → ((𝐴 ⊆ 𝑥 → 𝐴 ∈ V) ↔ (𝐴 ⊆ 𝐵 → 𝐴 ∈ V))) |
3 | vex 3435 | . . . 4 ⊢ 𝑥 ∈ V | |
4 | 3 | ssex 5249 | . . 3 ⊢ (𝐴 ⊆ 𝑥 → 𝐴 ∈ V) |
5 | 2, 4 | vtoclg 3504 | . 2 ⊢ (𝐵 ∈ 𝐶 → (𝐴 ⊆ 𝐵 → 𝐴 ∈ V)) |
6 | 5 | impcom 408 | 1 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝐶) → 𝐴 ∈ V) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 = wceq 1542 ∈ wcel 2110 Vcvv 3431 ⊆ wss 3892 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1917 ax-6 1975 ax-7 2015 ax-8 2112 ax-9 2120 ax-ext 2711 ax-sep 5227 |
This theorem depends on definitions: df-bi 206 df-an 397 df-tru 1545 df-ex 1787 df-sb 2072 df-clab 2718 df-cleq 2732 df-clel 2818 df-rab 3075 df-v 3433 df-in 3899 df-ss 3909 |
This theorem is referenced by: ssexd 5252 prcssprc 5253 difexg 5255 rabexg 5259 elssabg 5264 elpw2g 5272 abssexg 5309 snexALT 5310 sess1 5558 sess2 5559 riinint 5876 resexg 5936 trsuc 6349 ordsssuc2 6353 mptexg 7094 mptexgf 7095 isofr2 7211 ofres 7546 brrpssg 7572 unexb 7592 xpexg 7594 abnexg 7600 difex2 7604 uniexr 7607 dmexg 7744 rnexg 7745 resiexg 7755 imaexg 7756 exse2 7758 cnvexg 7765 coexg 7770 fabexg 7775 f1oabexg 7777 resfunexgALT 7784 cofunexg 7785 fnexALT 7787 f1dmex 7793 oprabexd 7811 mpoexxg 7909 suppfnss 7996 tposexg 8047 tz7.48-3 8266 oaabs 8461 erex 8505 mapex 8604 pmvalg 8609 elpmg 8614 elmapssres 8638 pmss12g 8640 ralxpmap 8667 ixpexg 8693 ssdomg 8769 fiprc 8818 domunsncan 8841 infensuc 8924 pssnn 8933 ssfi 8938 pssnnOLD 9018 unbnn 9048 fodomfi 9070 fival 9149 fiss 9161 dffi3 9168 hartogslem2 9280 card2on 9291 wdomima2g 9323 unxpwdom2 9325 unxpwdom 9326 harwdom 9328 oemapvali 9420 ackbij1lem11 9987 cofsmo 10026 ssfin4 10067 fin23lem11 10074 ssfin2 10077 ssfin3ds 10087 isfin1-3 10143 hsmex3 10191 axdc2lem 10205 ac6num 10236 ttukeylem1 10266 dmct 10281 ondomon 10320 fpwwe2lem3 10390 fpwwe2lem11 10398 fpwwe2lem12 10399 canthwe 10408 wuncss 10502 genpv 10756 genpdm 10759 hashss 14122 hashf1lem1OLD 14167 wrdexb 14226 shftfval 14779 o1of2 15320 o1rlimmul 15326 isercolllem2 15375 isstruct2 16848 ressval3d 16954 ressval3dOLD 16955 ressabs 16957 prdsbas 17166 fnmrc 17314 mrcfval 17315 isacs1i 17364 mreacs 17365 isssc 17530 ipolerval 18248 ress0g 18411 sylow2a 19222 islbs3 20415 toponsspwpw 22069 basdif0 22101 tgval 22103 eltg 22105 eltg2 22106 tgss 22116 basgen2 22137 2basgen 22138 bastop1 22141 topnex 22144 resttopon 22310 restabs 22314 restcld 22321 restfpw 22328 restcls 22330 restntr 22331 ordtbas2 22340 ordtbas 22341 lmfval 22381 cnrest 22434 cmpcov 22538 cmpsublem 22548 cmpsub 22549 2ndcomap 22607 islocfin 22666 txss12 22754 ptrescn 22788 trfbas2 22992 trfbas 22993 isfildlem 23006 snfbas 23015 trfil1 23035 trfil2 23036 trufil 23059 ssufl 23067 hauspwpwf1 23136 ustval 23352 metrest 23678 cnheibor 24116 metcld2 24469 bcthlem1 24486 mbfimaopn2 24819 0pledm 24835 dvbss 25063 dvreslem 25071 dvres2lem 25072 dvcnp2 25082 dvaddbr 25100 dvmulbr 25101 dvcnvrelem2 25180 elply2 25355 plyf 25357 plyss 25358 elplyr 25360 plyeq0lem 25369 plyeq0 25370 plyaddlem 25374 plymullem 25375 dgrlem 25388 coeidlem 25396 ulmcn 25556 pserulm 25579 rabexgfGS 30842 abrexdomjm 30848 aciunf1 30996 ress1r 31482 pcmplfin 31806 metidval 31836 indval 31977 sigagenss 32113 measval 32162 omsfval 32257 omssubaddlem 32262 omssubadd 32263 carsggect 32281 erdsze2lem1 33161 erdsze2lem2 33162 cvxpconn 33200 elmsta 33506 dfon2lem3 33757 altxpexg 34276 ivthALT 34520 filnetlem3 34565 bj-sselpwuni 35219 bj-elpwg 35221 bj-restsnss 35250 bj-restsnss2 35251 bj-restb 35261 bj-restuni2 35265 abrexdom 35884 sdclem2 35896 sdclem1 35897 imaexALTV 36461 brssr 36615 sticksstones4 40102 sticksstones14 40113 pssexg 40198 elrfirn 40514 pwssplit4 40911 hbtlem1 40945 hbtlem7 40947 inaex 41885 rabexgf 42537 dvnprodlem1 43458 dvnprodlem2 43459 qndenserrnbllem 43806 sge0ss 43921 psmeasurelem 43979 caragensplit 44009 omeunile 44014 caragenuncl 44022 omeunle 44025 omeiunlempt 44029 carageniuncllem2 44031 frnvafv2v 44696 prprval 44935 mpoexxg2 45642 gsumlsscl 45688 lincellss 45736 |
Copyright terms: Public domain | W3C validator |