Theorem sslin 4243

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

Syntax hints:   → wi 4   ∩ cin 3950   ⊆ wss 3951

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-rab 3437  df-v 3482  df-in 3958  df-ss 3968

This theorem is referenced by:  ss2in  4245  inxpssres  5702  ssres2  6022  predrelss  6358  sbthlem7  9129  kmlem5  10195  canthnum  10689  ioodisj  13522  hashun3  14423  dprdres  20048  dprd2da  20062  dmdprdsplit2lem  20065  srhmsubc  20680  rhmsubclem3  20687  fldc  20785  fldhmsubc  20786  cnprest  23297  isnrm3  23367  regsep2  23384  llycmpkgen2  23558  kqdisj  23740  regr1lem  23747  fclsbas  24029  fclscf  24033  flimfnfcls  24036  isfcf  24042  metdstri  24873  nulmbl2  25571  uniioombllem4  25621  volsup2  25640  volcn  25641  itg1climres  25749  limcresi  25920  limciun  25929  rlimcnp2  27009  rplogsum  27571  chssoc  31515  cmbr4i  31620  5oai  31680  3oalem6  31686  mdslmd4i  32352  atcvat4i  32416  imadifxp  32614  swrdrndisj  32942  1arithufdlem4  33575  crefss  33848  pnfneige0  33950  cldbnd  36327  neibastop1  36360  neibastop2  36362  onint1  36450  oninhaus  36451  bj-idres  37161  cntotbnd  37803  polcon3N  39919  osumcllem4N  39961  lcfrlem2  41545  mapfzcons1  42728  coeq0i  42764  eldioph4b  42822  icccncfext  45902  rhmsubcALTVlem4  48200  srhmsubcALTV  48241  fldcALTV  48248  fldhmsubcALTV  48249  ssdisjdr  48728  sepnsepolem2  48820