Theorem sslin 4198

Description: Add left intersection to subclass relation. (Contributed by NM, 19-Oct-1999.)

Assertion

Ref	Expression
sslin	⊢ (𝐴 ⊆ 𝐵 → (𝐶 ∩ 𝐴) ⊆ (𝐶 ∩ 𝐵))

Proof of Theorem sslin

Step	Hyp	Ref	Expression
1		ssrin 4197	. 2 ⊢ (𝐴 ⊆ 𝐵 → (𝐴 ∩ 𝐶) ⊆ (𝐵 ∩ 𝐶))
2		incom 4165	. 2 ⊢ (𝐶 ∩ 𝐴) = (𝐴 ∩ 𝐶)
3		incom 4165	. 2 ⊢ (𝐶 ∩ 𝐵) = (𝐵 ∩ 𝐶)
4	1, 2, 3	3sstr4g 3993	1 ⊢ (𝐴 ⊆ 𝐵 → (𝐶 ∩ 𝐴) ⊆ (𝐶 ∩ 𝐵))

This proof depends on syntax axioms:   → wi 4   ∩ cin 3907   ⊆ wss 3908

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2738

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2745  df-cleq 2758  df-clel 2841  df-rab 3420  df-v 3460  df-in 3915  df-ss 3925

This theorem is used by:  ss2in  4200  inxpssres  5683  ssres2  6008  predrelss  6345  sbthlem7  9091  kmlem5  10157  canthnum  10652  ioodisj  13527  hashun3  14440  dprdres  20131  dprd2da  20145  dmdprdsplit2lem  20148  srhmsubc  20816  rhmsubclem3  20823  fldc  20924  fldhmsubc  20925  cnprest  23483  isnrm3  23553  regsep2  23570  llycmpkgen2  23744  kqdisj  23926  regr1lem  23933  fclsbas  24215  fclscf  24219  flimfnfcls  24222  isfcf  24228  metdstri  25046  nulmbl2  25732  uniioombllem4  25782  volsup2  25801  volcn  25802  itg1climres  25910  limcresi  26081  limciun  26090  rlimcnp2  27168  rplogsum  27728  chssoc  31885  cmbr4i  31990  5oai  32050  3oalem6  32056  mdslmd4i  32722  atcvat4i  32786  imadifxp  32983  swrdrndisj  33308  1arithufdlem4  33868  crefss  34270  pnfneige0  34372  cldbnd  36878  neibastop1  36911  neibastop2  36913  onint1  37001  oninhaus  37002  bj-idres  37845  cntotbnd  38488  polcon3N  40732  osumcllem4N  40774  lcfrlem2  42358  mapfzcons1  43489  coeq0i  43525  eldioph4b  43579  icccncfext  46642  rhmsubcALTVlem4  49090  srhmsubcALTV  49131  fldcALTV  49138  fldhmsubcALTV  49139  ssdisjdr  49628  sepnsepolem2  49742