Theorem sslin 4251

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 4250	. 2 ⊢ (𝐴 ⊆ 𝐵 → (𝐴 ∩ 𝐶) ⊆ (𝐵 ∩ 𝐶))
2		incom 4217	. 2 ⊢ (𝐶 ∩ 𝐴) = (𝐴 ∩ 𝐶)
3		incom 4217	. 2 ⊢ (𝐶 ∩ 𝐵) = (𝐵 ∩ 𝐶)
4	1, 2, 3	3sstr4g 4041	1 ⊢ (𝐴 ⊆ 𝐵 → (𝐶 ∩ 𝐴) ⊆ (𝐶 ∩ 𝐵))

Syntax hints:   → wi 4   ∩ cin 3962   ⊆ wss 3963

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-rab 3434  df-v 3480  df-in 3970  df-ss 3980

This theorem is referenced by:  ss2in  4253  inxpssres  5706  ssres2  6025  predrelss  6360  sbthlem7  9128  kmlem5  10193  canthnum  10687  ioodisj  13519  hashun3  14420  dprdres  20063  dprd2da  20077  dmdprdsplit2lem  20080  srhmsubc  20697  rhmsubclem3  20704  fldc  20802  fldhmsubc  20803  cnprest  23313  isnrm3  23383  regsep2  23400  llycmpkgen2  23574  kqdisj  23756  regr1lem  23763  fclsbas  24045  fclscf  24049  flimfnfcls  24052  isfcf  24058  metdstri  24887  nulmbl2  25585  uniioombllem4  25635  volsup2  25654  volcn  25655  itg1climres  25764  limcresi  25935  limciun  25944  rlimcnp2  27024  rplogsum  27586  chssoc  31525  cmbr4i  31630  5oai  31690  3oalem6  31696  mdslmd4i  32362  atcvat4i  32426  imadifxp  32621  swrdrndisj  32927  1arithufdlem4  33555  crefss  33810  pnfneige0  33912  cldbnd  36309  neibastop1  36342  neibastop2  36344  onint1  36432  oninhaus  36433  bj-idres  37143  cntotbnd  37783  polcon3N  39900  osumcllem4N  39942  lcfrlem2  41526  mapfzcons1  42705  coeq0i  42741  eldioph4b  42799  icccncfext  45843  rhmsubcALTVlem4  48128  srhmsubcALTV  48169  fldcALTV  48176  fldhmsubcALTV  48177  ssdisjdr  48657  sepnsepolem2  48719