Theorem ssrin 4167

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 3914	. . . 4 ⊢ (𝐴 ⊆ 𝐵 → (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
2	1	anim1d 611	. . 3 ⊢ (𝐴 ⊆ 𝐵 → ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐶) → (𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶)))
3		elin 3903	. . 3 ⊢ (𝑥 ∈ (𝐴 ∩ 𝐶) ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐶))
4		elin 3903	. . 3 ⊢ (𝑥 ∈ (𝐵 ∩ 𝐶) ↔ (𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶))
5	2, 3, 4	3imtr4g 296	. 2 ⊢ (𝐴 ⊆ 𝐵 → (𝑥 ∈ (𝐴 ∩ 𝐶) → 𝑥 ∈ (𝐵 ∩ 𝐶)))
6	5	ssrdv 3927	1 ⊢ (𝐴 ⊆ 𝐵 → (𝐴 ∩ 𝐶) ⊆ (𝐵 ∩ 𝐶))

Syntax hints:   → wi 4   ∧ wa 396   ∈ wcel 2106   ∩ cin 3886   ⊆ wss 3887

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-v 3434  df-in 3894  df-ss 3904

This theorem is referenced by:  sslin  4168  ssrind  4169  ss2in  4170  ssdisj  4393  ssdifin0  4416  ssres  5918  predpredss  6209  sbthlem7  8876  onsdominel  8913  phplem2OLD  9001  infdifsn  9415  fin23lem23  10082  ttukeylem2  10266  limsupgord  15181  pjfval  20913  pjpm  20915  tgss  22118  neindisj2  22274  1stcrest  22604  kgencn3  22709  trfbas2  22994  fclsrest  23175  fcfnei  23186  cnextcn  23218  tsmsres  23295  trust  23381  restutopopn  23390  metrest  23680  reperflem  23981  ellimc3  25043  limcflf  25045  lhop1lem  25177  ppinprm  26301  chtnprm  26303  chtppilimlem1  26621  orthin  29808  3oalem6  30029  mdslle1i  30679  mdslle2i  30680  mdslj1i  30681  mdslj2i  30682  mdslmd1lem2  30688  mdslmd3i  30694  mdexchi  30697  eulerpartlemn  32348  poimirlem3  35780  poimirlem29  35806  ismblfin  35818  nnuzdisj  42894  sumnnodd  43171  liminfgord  43295  sge0less  43930  sepnsepo  46217