![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > ssind | Structured version Visualization version Unicode 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 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | ssind.2 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | ssin 3666 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 3 | biimpi 199 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
5 | 1, 2, 4 | syl2anc 671 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1680 ax-4 1693 ax-5 1769 ax-6 1816 ax-7 1862 ax-10 1926 ax-11 1931 ax-12 1944 ax-13 2102 ax-ext 2442 |
This theorem depends on definitions: df-bi 190 df-an 377 df-tru 1458 df-ex 1675 df-nf 1679 df-sb 1809 df-clab 2449 df-cleq 2455 df-clel 2458 df-nfc 2592 df-v 3059 df-in 3423 df-ss 3430 |
This theorem is referenced by: mreexexlem3d 15601 isacs1i 15612 rescabs 15787 funcres2c 15855 lsmmod 17374 gsumzres 17592 gsumzsubmcl 17600 gsum2d 17653 issubdrg 18082 lspdisj 18397 mplind 18774 ntrin 20125 elcls 20138 neitr 20245 restcls 20246 lmss 20363 xkoinjcn 20751 trfg 20955 trust 21293 utoptop 21298 restutop 21301 isngp2 21660 lebnumii 22046 causs 22317 dvreslem 22913 c1lip3 23000 ssjo 27149 dmdbr5 28010 mdslj2i 28022 mdsl2bi 28025 mdslmd1lem2 28028 mdsymlem5 28109 bnj1286 29877 mclsind 30257 neiin 31037 topmeet 31069 fnemeet2 31072 pmod1i 33458 dihmeetlem1N 34903 dihglblem5apreN 34904 dochdmj1 35003 mapdin 35275 baerlem3lem2 35323 baerlem5alem2 35324 baerlem5blem2 35325 trrelind 36302 nzin 36711 islptre 37737 limccog 37738 limcresiooub 37761 limcresioolb 37762 fourierdlem48 38056 fourierdlem49 38057 fourierdlem113 38121 |
Copyright terms: Public domain | W3C validator |