![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > ssinss1 | Structured version Visualization version GIF version |
Description: Intersection preserves subclass relationship. (Contributed by NM, 14-Sep-1999.) |
Ref | Expression |
---|---|
ssinss1 | ⊢ (𝐴 ⊆ 𝐶 → (𝐴 ∩ 𝐵) ⊆ 𝐶) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | inss1 4228 | . 2 ⊢ (𝐴 ∩ 𝐵) ⊆ 𝐴 | |
2 | sstr2 3989 | . 2 ⊢ ((𝐴 ∩ 𝐵) ⊆ 𝐴 → (𝐴 ⊆ 𝐶 → (𝐴 ∩ 𝐵) ⊆ 𝐶)) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ (𝐴 ⊆ 𝐶 → (𝐴 ∩ 𝐵) ⊆ 𝐶) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∩ cin 3947 ⊆ wss 3948 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1912 ax-6 1970 ax-7 2010 ax-8 2107 ax-9 2115 ax-ext 2702 |
This theorem depends on definitions: df-bi 206 df-an 396 df-tru 1543 df-ex 1781 df-sb 2067 df-clab 2709 df-cleq 2723 df-clel 2809 df-v 3475 df-in 3955 df-ss 3965 |
This theorem is referenced by: inss 4238 wfrlem4OLD 8318 wfrlem5OLD 8319 fipwuni 9427 ssfin4 10311 insubm 18741 distop 22818 fctop 22827 cctop 22829 ntrin 22885 innei 22949 lly1stc 23320 txcnp 23444 isfild 23682 utoptop 24059 restmetu 24399 lecmi 31289 mdslj2i 32007 mdslmd1lem1 32012 mdslmd1lem2 32013 elpwincl1 32197 pnfneige0 33396 inelcarsg 33775 ballotlemfrc 33990 bnj1177 34482 bnj1311 34500 cldbnd 35677 neiin 35683 ontgval 35782 mblfinlem4 36994 pmodlem1 39183 pmodlem2 39184 pmod1i 39185 pmod2iN 39186 pmodl42N 39188 dochdmj1 40727 ssficl 42785 ntrclskb 43285 ntrclsk13 43287 ntrneik3 43312 ntrneik13 43314 ssinss1d 44199 icccncfext 45064 fourierdlem48 45331 fourierdlem49 45332 fourierdlem113 45396 caragendifcl 45691 omelesplit 45695 carageniuncllem2 45699 carageniuncl 45700 |
Copyright terms: Public domain | W3C validator |