Theorem sslin 4139

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

This proof depends on syntax axioms:   → wi 4   ⊆ wss 3895   ∩ cin 4089

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-ss 3896  df-in 4091

This theorem is used by:  ss2in  4141  inxpssres  5667  ssres2  5994  predrelss  6340  sbthlem7  9115  kmlem5  10236  canthnum  10737  ioodisj  13616  hashun3  14531  dprdres  20249  dprd2da  20263  dmdprdsplit2lem  20266  srhmsubc  20937  rhmsubclem3  20944  fldc  21046  fldhmsubc  21047  cnprest  23612  isnrm3  23682  regsep2  23699  llycmpkgen2  23874  kqdisj  24056  regr1lem  24063  fclsbas  24345  fclscf  24349  flimfnfcls  24352  isfcf  24358  metdstri  25176  nulmbl2  25862  uniioombllem4  25912  volsup2  25931  volcn  25932  itg1climres  26040  limcresi  26210  limciun  26219  rlimcnp2  27299  rplogsum  27859  chssoc  32103  cmbr4i  32208  5oai  32268  3oalem6  32274  mdslmd4i  32940  atcvat4i  33004  imadifxp  33242  swrdrndisj  33564  1arithufdlem4  34125  crefss  34527  pnfneige0  34629  cldbnd  37206  neibastop1  37239  neibastop2  37241  onint1  37329  oninhaus  37330  bj-idres  38174  cntotbnd  38823  polcon3N  41067  osumcllem4N  41109  lcfrlem2  42693  mapfzcons1  43821  coeq0i  43857  eldioph4b  43911  icccncfext  46990  rhmsubcALTVlem4  49474  srhmsubcALTV  49515  fldcALTV  49522  fldhmsubcALTV  49523  ssdisjdr  50012  sepnsepolem2  50130