![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > ssind | Structured version Visualization version GIF version |
Description: A deduction showing that a subclass of two classes is a subclass of their intersection. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) |
Ref | Expression |
---|---|
ssind.1 | ⊢ (𝜑 → 𝐴 ⊆ 𝐵) |
ssind.2 | ⊢ (𝜑 → 𝐴 ⊆ 𝐶) |
Ref | Expression |
---|---|
ssind | ⊢ (𝜑 → 𝐴 ⊆ (𝐵 ∩ 𝐶)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ssind.1 | . . 3 ⊢ (𝜑 → 𝐴 ⊆ 𝐵) | |
2 | ssind.2 | . . 3 ⊢ (𝜑 → 𝐴 ⊆ 𝐶) | |
3 | 1, 2 | jca 510 | . 2 ⊢ (𝜑 → (𝐴 ⊆ 𝐵 ∧ 𝐴 ⊆ 𝐶)) |
4 | ssin 4229 | . 2 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐴 ⊆ 𝐶) ↔ 𝐴 ⊆ (𝐵 ∩ 𝐶)) | |
5 | 3, 4 | sylib 217 | 1 ⊢ (𝜑 → 𝐴 ⊆ (𝐵 ∩ 𝐶)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 394 ∩ cin 3943 ⊆ wss 3944 |
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 |
This theorem depends on definitions: df-bi 206 df-an 395 df-tru 1536 df-ex 1774 df-sb 2060 df-clab 2703 df-cleq 2717 df-clel 2802 df-v 3463 df-in 3951 df-ss 3961 |
This theorem is referenced by: frrlem12 8303 frrlem13 8304 mreexexlem3d 17629 isacs1i 17640 rescabs 17821 rescabsOLD 17822 funcres2c 17893 lsmmod 19642 gsumzres 19876 gsumzsubmcl 19885 gsum2d 19939 issubdrg 20680 lspdisj 21025 mplind 22036 ntrin 23009 elcls 23021 neitr 23128 restcls 23129 lmss 23246 xkoinjcn 23635 trfg 23839 trust 24178 utoptop 24183 restutop 24186 isngp2 24550 lebnumii 24936 causs 25270 dvreslem 25882 c1lip3 25976 ssjo 31329 dmdbr5 32190 mdslj2i 32202 mdsl2bi 32205 mdslmd1lem2 32208 mdsymlem5 32289 difininv 32392 idlsrgmulrssin 33325 bnj1286 34781 mclsind 35311 neiin 35947 topmeet 35979 fnemeet2 35982 bj-elpwg 36662 bj-restpw 36702 bj-restb 36704 bj-restuni2 36708 idresssidinxp 37910 pmod1i 39451 dihmeetlem1N 40893 dihglblem5apreN 40894 dochdmj1 40993 mapdin 41265 baerlem3lem2 41313 baerlem5alem2 41314 baerlem5blem2 41315 trrelind 43237 isotone2 43621 nzin 43897 inmap 44721 islptre 45145 limccog 45146 limcresiooub 45168 limcresioolb 45169 limsupresxr 45292 liminfresxr 45293 liminfvalxr 45309 fourierdlem48 45680 fourierdlem49 45681 fourierdlem113 45745 pimiooltgt 46236 pimdecfgtioc 46241 pimincfltioc 46242 pimdecfgtioo 46243 pimincfltioo 46244 sssmf 46264 smflimlem2 46298 smfsuplem1 46337 iscnrm3llem2 48155 setrec2fun 48309 |
Copyright terms: Public domain | W3C validator |