Theorem ssrin 4148

Description: Add right intersection to subclass relation. (Contributed by NM, 16-Aug-1994.) (Proof shortened by Andrew Salmon, 26-Jun-2011.)

Assertion

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

Proof of Theorem ssrin

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		ssel 3893	. . . 4 ⊢ (𝐴 ⊆ 𝐵 → (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
2	1	anim1d 614	. . 3 ⊢ (𝐴 ⊆ 𝐵 → ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐶) → (𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶)))
3		elin 3882	. . 3 ⊢ (𝑥 ∈ (𝐴 ∩ 𝐶) ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐶))
4		elin 3882	. . 3 ⊢ (𝑥 ∈ (𝐵 ∩ 𝐶) ↔ (𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶))
5	2, 3, 4	3imtr4g 299	. 2 ⊢ (𝐴 ⊆ 𝐵 → (𝑥 ∈ (𝐴 ∩ 𝐶) → 𝑥 ∈ (𝐵 ∩ 𝐶)))
6	5	ssrdv 3907	1 ⊢ (𝐴 ⊆ 𝐵 → (𝐴 ∩ 𝐶) ⊆ (𝐵 ∩ 𝐶))

Syntax hints:   → wi 4   ∧ wa 399   ∈ wcel 2110   ∩ cin 3865   ⊆ wss 3866

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1546  df-ex 1788  df-sb 2071  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3410  df-in 3873  df-ss 3883

This theorem is referenced by:  sslin  4149  ssrind  4150  ss2in  4151  ssdisj  4374  ssdifin0  4397  ssres  5878  predpredss  6166  sbthlem7  8762  onsdominel  8795  phplem2  8826  infdifsn  9272  fin23lem23  9940  ttukeylem2  10124  limsupgord  15033  pjfval  20668  pjpm  20670  tgss  21865  neindisj2  22020  1stcrest  22350  kgencn3  22455  trfbas2  22740  fclsrest  22921  fcfnei  22932  cnextcn  22964  tsmsres  23041  trust  23127  restutopopn  23136  metrest  23422  reperflem  23715  ellimc3  24776  limcflf  24778  lhop1lem  24910  ppinprm  26034  chtnprm  26036  chtppilimlem1  26354  orthin  29527  3oalem6  29748  mdslle1i  30398  mdslle2i  30399  mdslj1i  30400  mdslj2i  30401  mdslmd1lem2  30407  mdslmd3i  30413  mdexchi  30416  eulerpartlemn  32060  poimirlem3  35517  poimirlem29  35543  ismblfin  35555  nnuzdisj  42567  sumnnodd  42846  liminfgord  42970  sge0less  43605  sepnsepo  45890