| 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 4237 | . 2 ⊢ (𝐴 ∩ 𝐵) ⊆ 𝐴 | |
| 2 | sstr2 3990 | . 2 ⊢ ((𝐴 ∩ 𝐵) ⊆ 𝐴 → (𝐴 ⊆ 𝐶 → (𝐴 ∩ 𝐵) ⊆ 𝐶)) | |
| 3 | 1, 2 | ax-mp 5 | 1 ⊢ (𝐴 ⊆ 𝐶 → (𝐴 ∩ 𝐵) ⊆ 𝐶) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∩ cin 3950 ⊆ wss 3951 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-tru 1543 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-v 3482 df-in 3958 df-ss 3968 |
| This theorem is referenced by: ssinss1d 4247 inss 4248 inindif 4375 wfrlem4OLD 8352 wfrlem5OLD 8353 fipwuni 9466 ssfin4 10350 insubm 18831 distop 23002 fctop 23011 cctop 23013 ntrin 23069 innei 23133 lly1stc 23504 txcnp 23628 isfild 23866 utoptop 24243 restmetu 24583 lecmi 31621 mdslj2i 32339 mdslmd1lem1 32344 mdslmd1lem2 32345 elpwincl1 32544 pnfneige0 33950 inelcarsg 34313 ballotlemfrc 34529 bnj1177 35020 bnj1311 35038 cldbnd 36327 neiin 36333 ontgval 36432 mblfinlem4 37667 pmodlem1 39848 pmodlem2 39849 pmod1i 39850 pmod2iN 39851 pmodl42N 39853 dochdmj1 41392 redvmptabs 42390 ssficl 43582 ntrclskb 44082 ntrclsk13 44084 ntrneik3 44109 ntrneik13 44111 sswfaxreg 45004 icccncfext 45902 fourierdlem48 46169 fourierdlem49 46170 fourierdlem113 46234 caragendifcl 46529 omelesplit 46533 carageniuncllem2 46537 carageniuncl 46538 |
| Copyright terms: Public domain | W3C validator |