![]() |
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 507 | . 2 ⊢ (𝜑 → (𝐴 ⊆ 𝐵 ∧ 𝐴 ⊆ 𝐶)) |
4 | ssin 4061 | . 2 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐴 ⊆ 𝐶) ↔ 𝐴 ⊆ (𝐵 ∩ 𝐶)) | |
5 | 3, 4 | sylib 210 | 1 ⊢ (𝜑 → 𝐴 ⊆ (𝐵 ∩ 𝐶)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 386 ∩ cin 3797 ⊆ wss 3798 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1894 ax-4 1908 ax-5 2009 ax-6 2075 ax-7 2112 ax-9 2173 ax-10 2192 ax-11 2207 ax-12 2220 ax-ext 2803 |
This theorem depends on definitions: df-bi 199 df-an 387 df-or 879 df-tru 1660 df-ex 1879 df-nf 1883 df-sb 2068 df-clab 2812 df-cleq 2818 df-clel 2821 df-nfc 2958 df-v 3416 df-in 3805 df-ss 3812 |
This theorem is referenced by: mreexexlem3d 16666 isacs1i 16677 rescabs 16852 funcres2c 16920 lsmmod 18446 gsumzres 18670 gsumzsubmcl 18678 gsum2d 18731 issubdrg 19168 lspdisj 19491 mplind 19869 ntrin 21243 elcls 21255 neitr 21362 restcls 21363 lmss 21480 xkoinjcn 21868 trfg 22072 trust 22410 utoptop 22415 restutop 22418 isngp2 22778 lebnumii 23142 causs 23473 dvreslem 24079 c1lip3 24168 ssjo 28857 dmdbr5 29718 mdslj2i 29730 mdsl2bi 29733 mdslmd1lem2 29736 mdsymlem5 29817 difininv 29898 bnj1286 31629 mclsind 32009 neiin 32860 topmeet 32892 fnemeet2 32895 bj-restpw 33567 bj-restb 33569 bj-restuni2 33573 idresssidinxp 34627 pmod1i 35922 dihmeetlem1N 37364 dihglblem5apreN 37365 dochdmj1 37464 mapdin 37736 baerlem3lem2 37784 baerlem5alem2 37785 baerlem5blem2 37786 trrelind 38797 isotone2 39186 nzin 39356 inmap 40206 islptre 40644 limccog 40645 limcresiooub 40667 limcresioolb 40668 limsupresxr 40791 liminfresxr 40792 liminfvalxr 40808 fourierdlem48 41163 fourierdlem49 41164 fourierdlem113 41228 pimiooltgt 41713 pimdecfgtioc 41717 pimincfltioc 41718 pimdecfgtioo 41719 pimincfltioo 41720 sssmf 41739 smflimlem2 41772 smfsuplem1 41809 setrec2fun 43348 |
Copyright terms: Public domain | W3C validator |