![]() |
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 4005 | . . . 4 ⊢ (𝑥 = 𝐵 → (𝐴 ⊆ 𝑥 ↔ 𝐴 ⊆ 𝐵)) | |
2 | 1 | imbi1d 340 | . . 3 ⊢ (𝑥 = 𝐵 → ((𝐴 ⊆ 𝑥 → 𝐴 ∈ V) ↔ (𝐴 ⊆ 𝐵 → 𝐴 ∈ V))) |
3 | vex 3465 | . . . 4 ⊢ 𝑥 ∈ V | |
4 | 3 | ssex 5325 | . . 3 ⊢ (𝐴 ⊆ 𝑥 → 𝐴 ∈ V) |
5 | 2, 4 | vtoclg 3533 | . 2 ⊢ (𝐵 ∈ 𝐶 → (𝐴 ⊆ 𝐵 → 𝐴 ∈ V)) |
6 | 5 | impcom 406 | 1 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝐶) → 𝐴 ∈ V) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 394 = wceq 1533 ∈ wcel 2098 Vcvv 3461 ⊆ wss 3946 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-ext 2696 ax-sep 5303 |
This theorem depends on definitions: df-bi 206 df-an 395 df-3an 1086 df-tru 1536 df-ex 1774 df-sb 2060 df-clab 2703 df-cleq 2717 df-clel 2802 df-rab 3419 df-v 3463 df-in 3953 df-ss 3963 |
This theorem is referenced by: ssexd 5328 prcssprc 5331 difexg 5333 rabexg 5337 elssabg 5342 elpw2g 5350 abssexg 5385 snexALT 5386 sess1 5649 sess2 5650 riinint 5974 resexg 6035 trsuc 6462 ordsssuc2 6466 mptexg 7237 mptexgf 7238 isofr2 7355 ofres 7708 brrpssg 7735 unexb 7755 xpexg 7757 abnexg 7763 difex2 7767 uniexr 7770 dmexg 7913 rnexg 7914 resiexg 7924 imaexg 7925 exse2 7929 cnvexg 7936 coexg 7941 fabexgOLD 7949 f1oabexgOLD 7953 resfunexgALT 7960 cofunexg 7961 fnexALT 7963 f1dmex 7969 oprabexd 7988 mpoexxg 8088 suppfnss 8202 tposexg 8254 tz7.48-3 8473 oaabs 8677 erex 8757 mapexOLD 8860 pmvalg 8865 elpmg 8871 elmapssres 8895 pmss12g 8897 ralxpmap 8924 ixpexg 8950 domssl 9028 ssdomg 9030 fiprc 9082 domunsncan 9109 infensuc 9192 pssnn 9205 ssfi 9210 pssnnOLD 9302 enp1i 9316 unbnn 9336 fodomfi 9365 fival 9451 fiss 9463 dffi3 9470 hartogslem2 9582 card2on 9593 wdomima2g 9625 unxpwdom2 9627 unxpwdom 9628 harwdom 9630 oemapvali 9723 ackbij1lem11 10269 cofsmo 10308 ssfin4 10349 fin23lem11 10356 ssfin2 10359 ssfin3ds 10369 isfin1-3 10425 hsmex3 10473 axdc2lem 10487 ac6num 10518 ttukeylem1 10548 dmct 10563 ondomon 10602 fpwwe2lem3 10672 fpwwe2lem11 10680 fpwwe2lem12 10681 canthwe 10690 wuncss 10784 genpv 11038 genpdm 11041 hashss 14421 hashf1lem1OLD 14469 wrdexb 14528 shftfval 15070 o1of2 15610 o1rlimmul 15616 isercolllem2 15665 isstruct2 17146 ressval3d 17255 ressval3dOLD 17256 ressabs 17258 prdsbas 17467 fnmrc 17615 mrcfval 17616 isacs1i 17665 mreacs 17666 isssc 17831 ipolerval 18552 ress0g 18750 sylow2a 19612 islbs3 21083 toponsspwpw 22907 basdif0 22939 tgval 22941 eltg 22943 eltg2 22944 tgss 22954 basgen2 22975 2basgen 22976 bastop1 22979 topnex 22982 resttopon 23148 restabs 23152 restcld 23159 restfpw 23166 restcls 23168 restntr 23169 ordtbas2 23178 ordtbas 23179 lmfval 23219 cnrest 23272 cmpcov 23376 cmpsublem 23386 cmpsub 23387 2ndcomap 23445 islocfin 23504 txss12 23592 ptrescn 23626 trfbas2 23830 trfbas 23831 isfildlem 23844 snfbas 23853 trfil1 23873 trfil2 23874 trufil 23897 ssufl 23905 hauspwpwf1 23974 ustval 24190 metrest 24516 cnheibor 24964 metcld2 25318 bcthlem1 25335 mbfimaopn2 25669 0pledm 25685 dvbss 25913 dvreslem 25921 dvres2lem 25922 dvcnp2 25932 dvcnp2OLD 25933 dvaddbr 25951 dvmulbr 25952 dvmulbrOLD 25953 dvcnvrelem2 26034 elply2 26215 plyf 26217 plyss 26218 elplyr 26220 plyeq0lem 26229 plyeq0 26230 plyaddlem 26234 plymullem 26235 dgrlem 26248 coeidlem 26256 ulmcn 26420 pserulm 26443 rabexgfGS 32418 abrexdomjm 32423 aciunf1 32571 ress1r 33076 pcmplfin 33631 metidval 33661 indval 33802 sigagenss 33938 measval 33987 omsfval 34084 omssubaddlem 34089 omssubadd 34090 carsggect 34108 erdsze2lem1 34983 erdsze2lem2 34984 cvxpconn 35022 elmsta 35328 dfon2lem3 35557 altxpexg 35750 ivthALT 35995 filnetlem3 36040 bj-sselpwuni 36705 bj-elpwg 36707 bj-restsnss 36738 bj-restsnss2 36739 bj-restb 36749 bj-restuni2 36753 abrexdom 37379 sdclem2 37391 sdclem1 37392 imaexALTV 37976 brssr 38147 sticksstones4 41795 sticksstones14 41806 pssexg 41891 elrfirn 42289 pwssplit4 42687 hbtlem1 42721 hbtlem7 42723 inaex 43908 rabexgf 44560 dvnprodlem1 45504 dvnprodlem2 45505 qndenserrnbllem 45852 sge0ss 45970 psmeasurelem 46028 caragensplit 46058 omeunile 46063 caragenuncl 46071 omeunle 46074 omeiunlempt 46078 carageniuncllem2 46080 fcdmvafv2v 46786 prprval 47023 mpoexxg2 47653 gsumlsscl 47699 lincellss 47746 |
Copyright terms: Public domain | W3C validator |