![]() |
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 4192 | . 2 ⊢ (𝐴 ⊆ 𝐵 → (𝐴 ∩ 𝐶) ⊆ (𝐵 ∩ 𝐶)) | |
2 | sslin 4193 | . 2 ⊢ (𝐶 ⊆ 𝐷 → (𝐵 ∩ 𝐶) ⊆ (𝐵 ∩ 𝐷)) | |
3 | 1, 2 | sylan9ss 3956 | 1 ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐷) → (𝐴 ∩ 𝐶) ⊆ (𝐵 ∩ 𝐷)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 ∩ cin 3908 ⊆ wss 3909 |
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 2707 |
This theorem depends on definitions: df-bi 206 df-an 397 df-tru 1544 df-ex 1782 df-sb 2068 df-clab 2714 df-cleq 2728 df-clel 2814 df-rab 3407 df-v 3446 df-in 3916 df-ss 3926 |
This theorem is referenced by: disjxiun 5101 f1un 6802 undomOLD 9001 strleun 17026 dprdss 19804 dprd2da 19817 ablfac1b 19845 tgcl 22315 innei 22472 hausnei2 22700 bwth 22757 fbssfi 23184 fbunfip 23216 fgcl 23225 blin2 23778 vtxdun 28327 vtxdginducedm1 28389 5oai 30501 mayetes3i 30569 mdsl0 31150 neibastop1 34820 ismblfin 36108 heibor1lem 36257 pl42lem2N 38432 pl42lem3N 38433 ntrk2imkb 42289 ssin0 43243 iscnrm3llem2 46953 |
Copyright terms: Public domain | W3C validator |