![]() |
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 4087 | . 2 ⊢ (𝐴 ∩ 𝐵) ⊆ 𝐴 | |
2 | sstr2 3861 | . 2 ⊢ ((𝐴 ∩ 𝐵) ⊆ 𝐴 → (𝐴 ⊆ 𝐶 → (𝐴 ∩ 𝐵) ⊆ 𝐶)) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ (𝐴 ⊆ 𝐶 → (𝐴 ∩ 𝐵) ⊆ 𝐶) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∩ cin 3824 ⊆ wss 3825 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1758 ax-4 1772 ax-5 1869 ax-6 1928 ax-7 1964 ax-8 2050 ax-9 2057 ax-10 2077 ax-11 2091 ax-12 2104 ax-ext 2745 |
This theorem depends on definitions: df-bi 199 df-an 388 df-or 834 df-tru 1510 df-ex 1743 df-nf 1747 df-sb 2014 df-clab 2754 df-cleq 2765 df-clel 2840 df-nfc 2912 df-v 3411 df-in 3832 df-ss 3839 |
This theorem is referenced by: inss 4097 wfrlem4 7754 wfrlem4OLD 7755 wfrlem5 7756 fipwuni 8677 ssfin4 9522 distop 21297 fctop 21306 cctop 21308 ntrin 21363 innei 21427 lly1stc 21798 txcnp 21922 isfild 22160 utoptop 22536 restmetu 22873 lecmi 29150 mdslj2i 29868 mdslmd1lem1 29873 mdslmd1lem2 29874 elpwincl1 30050 pnfneige0 30795 inelcarsg 31171 ballotlemfrc 31387 bnj1177 31884 bnj1311 31902 cldbnd 33135 neiin 33141 ontgval 33239 mblfinlem4 34321 pmodlem1 36375 pmodlem2 36376 pmod1i 36377 pmod2iN 36378 pmodl42N 36380 dochdmj1 37919 ssficl 39235 ntrclskb 39727 ntrclsk13 39729 ntrneik3 39754 ntrneik13 39756 ssinss1d 40673 icccncfext 41546 fourierdlem48 41816 fourierdlem49 41817 fourierdlem113 41881 caragendifcl 42173 omelesplit 42177 carageniuncllem2 42181 carageniuncl 42182 |
Copyright terms: Public domain | W3C validator |