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 3991 | . . . 4 ⊢ (𝑥 = 𝐵 → (𝐴 ⊆ 𝑥 ↔ 𝐴 ⊆ 𝐵)) | |
2 | 1 | imbi1d 344 | . . 3 ⊢ (𝑥 = 𝐵 → ((𝐴 ⊆ 𝑥 → 𝐴 ∈ V) ↔ (𝐴 ⊆ 𝐵 → 𝐴 ∈ V))) |
3 | vex 3496 | . . . 4 ⊢ 𝑥 ∈ V | |
4 | 3 | ssex 5216 | . . 3 ⊢ (𝐴 ⊆ 𝑥 → 𝐴 ∈ V) |
5 | 2, 4 | vtoclg 3566 | . 2 ⊢ (𝐵 ∈ 𝐶 → (𝐴 ⊆ 𝐵 → 𝐴 ∈ V)) |
6 | 5 | impcom 410 | 1 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝐶) → 𝐴 ∈ V) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 398 = wceq 1531 ∈ wcel 2108 Vcvv 3493 ⊆ wss 3934 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1905 ax-6 1964 ax-7 2009 ax-8 2110 ax-9 2118 ax-10 2139 ax-11 2154 ax-12 2170 ax-ext 2791 ax-sep 5194 |
This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-tru 1534 df-ex 1775 df-nf 1779 df-sb 2064 df-clab 2798 df-cleq 2812 df-clel 2891 df-nfc 2961 df-rab 3145 df-v 3495 df-in 3941 df-ss 3950 |
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 6976 mptexgf 6977 isofr2 7089 ofres 7417 brrpssg 7443 unexb 7463 xpexg 7465 abnexg 7470 difex2 7474 uniexr 7477 dmexg 7605 rnexg 7606 resiexg 7611 imaexg 7612 exse2 7614 cnvexg 7621 coexg 7626 fabexg 7631 f1oabexg 7634 resfunexgALT 7641 cofunexg 7642 fnexALT 7644 f1dmex 7650 oprabexd 7668 mpoexxg 7765 suppfnss 7847 tposexg 7898 tz7.48-3 8072 oaabs 8263 erex 8305 mapex 8404 pmvalg 8409 elpmg 8414 elmapssres 8423 pmss12g 8425 ralxpmap 8452 ixpexg 8478 ssdomg 8547 fiprc 8587 domunsncan 8609 infensuc 8687 pssnn 8728 unbnn 8766 fodomfi 8789 fival 8868 fiss 8880 dffi3 8887 hartogslem2 8999 card2on 9010 wdomima2g 9042 unxpwdom2 9044 unxpwdom 9045 harwdom 9046 oemapvali 9139 ackbij1lem11 9644 cofsmo 9683 ssfin4 9724 fin23lem11 9731 ssfin2 9734 ssfin3ds 9744 isfin1-3 9800 hsmex3 9848 axdc2lem 9862 ac6num 9893 ttukeylem1 9923 dmct 9938 ondomon 9977 fpwwe2lem3 10047 fpwwe2lem12 10055 fpwwe2lem13 10056 canthwe 10065 wuncss 10159 genpv 10413 genpdm 10416 hashss 13762 hashf1lem1 13805 wrdexgOLD 13864 wrdexb 13865 shftfval 14421 o1of2 14961 o1rlimmul 14967 isercolllem2 15014 isstruct2 16485 ressval3d 16553 ressabs 16555 prdsbas 16722 fnmrc 16870 mrcfval 16871 isacs1i 16920 mreacs 16921 isssc 17082 ipolerval 17758 ress0g 17931 sylow2a 18736 islbs3 19919 toponsspwpw 21522 basdif0 21553 tgval 21555 eltg 21557 eltg2 21558 tgss 21568 basgen2 21589 2basgen 21590 bastop1 21593 topnex 21596 resttopon 21761 restabs 21765 restcld 21772 restfpw 21779 restcls 21781 restntr 21782 ordtbas2 21791 ordtbas 21792 lmfval 21832 cnrest 21885 cmpcov 21989 cmpsublem 21999 cmpsub 22000 2ndcomap 22058 islocfin 22117 txss12 22205 ptrescn 22239 trfbas2 22443 trfbas 22444 isfildlem 22457 snfbas 22466 trfil1 22486 trfil2 22487 trufil 22510 ssufl 22518 hauspwpwf1 22587 ustval 22803 metrest 23126 cnheibor 23551 metcld2 23902 bcthlem1 23919 mbfimaopn2 24250 0pledm 24266 dvbss 24491 dvreslem 24499 dvres2lem 24500 dvcnp2 24509 dvaddbr 24527 dvmulbr 24528 dvcnvrelem2 24607 elply2 24778 plyf 24780 plyss 24781 elplyr 24783 plyeq0lem 24792 plyeq0 24793 plyaddlem 24797 plymullem 24798 dgrlem 24811 coeidlem 24819 ulmcn 24979 pserulm 25002 rabexgfGS 30254 abrexdomjm 30259 aciunf1 30400 ress1r 30853 pcmplfin 31117 metidval 31123 indval 31265 sigagenss 31401 measval 31450 omsfval 31545 omssubaddlem 31550 omssubadd 31551 carsggect 31569 erdsze2lem1 32443 erdsze2lem2 32444 cvxpconn 32482 elmsta 32788 dfon2lem3 33023 altxpexg 33432 ivthALT 33676 filnetlem3 33721 bj-sselpwuni 34335 bj-elpwg 34337 bj-restsnss 34366 bj-restsnss2 34367 bj-restb 34377 bj-restuni2 34381 abrexdom 34997 sdclem2 35009 sdclem1 35010 imaexALTV 35579 brssr 35733 pssexg 39103 elrfirn 39283 pwssplit4 39680 hbtlem1 39714 hbtlem7 39716 inaex 40624 rabexgf 41272 disjinfi 41444 dvnprodlem1 42221 dvnprodlem2 42222 qndenserrnbllem 42570 sge0ss 42685 psmeasurelem 42743 caragensplit 42773 omeunile 42778 caragenuncl 42786 omeunle 42789 omeiunlempt 42793 carageniuncllem2 42795 frnvafv2v 43426 prprval 43667 mpoexxg2 44377 gsumlsscl 44422 lincellss 44472 |
Copyright terms: Public domain | W3C validator |