![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > ss2in | Structured version Visualization version GIF version |
Description: Intersection of subclasses. (Contributed by NM, 5-May-2000.) |
Ref | Expression |
---|---|
ss2in | ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐷) → (𝐴 ∩ 𝐶) ⊆ (𝐵 ∩ 𝐷)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ssrin 4198 | . 2 ⊢ (𝐴 ⊆ 𝐵 → (𝐴 ∩ 𝐶) ⊆ (𝐵 ∩ 𝐶)) | |
2 | sslin 4199 | . 2 ⊢ (𝐶 ⊆ 𝐷 → (𝐵 ∩ 𝐶) ⊆ (𝐵 ∩ 𝐷)) | |
3 | 1, 2 | sylan9ss 3960 | 1 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐷) → (𝐴 ∩ 𝐶) ⊆ (𝐵 ∩ 𝐷)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 ∩ cin 3912 ⊆ wss 3913 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-ext 2702 |
This theorem depends on definitions: df-bi 206 df-an 397 df-tru 1544 df-ex 1782 df-sb 2068 df-clab 2709 df-cleq 2723 df-clel 2809 df-rab 3406 df-v 3448 df-in 3920 df-ss 3930 |
This theorem is referenced by: disjxiun 5107 f1un 6809 undomOLD 9011 strleun 17040 dprdss 19822 dprd2da 19835 ablfac1b 19863 tgcl 22356 innei 22513 hausnei2 22741 bwth 22798 fbssfi 23225 fbunfip 23257 fgcl 23266 blin2 23819 vtxdun 28492 vtxdginducedm1 28554 5oai 30666 mayetes3i 30734 mdsl0 31315 neibastop1 34907 ismblfin 36192 heibor1lem 36341 pl42lem2N 38516 pl42lem3N 38517 ntrk2imkb 42431 ssin0 43385 iscnrm3llem2 47103 |
Copyright terms: Public domain | W3C validator |