Theorem ssrin 4263

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2108   ∩ cin 3975   ⊆ wss 3976

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-v 3490  df-in 3983  df-ss 3993

This theorem is referenced by:  sslin  4264  ssrind  4265  ss2in  4266  ssdisj  4483  ssdifin0  4509  ssres  6033  predpredss  6339  sbthlem7  9155  onsdominel  9192  phplem2OLD  9281  infdifsn  9726  fin23lem23  10395  ttukeylem2  10579  limsupgord  15518  pjfval  21749  pjpm  21751  tgss  22996  neindisj2  23152  1stcrest  23482  kgencn3  23587  trfbas2  23872  fclsrest  24053  fcfnei  24064  cnextcn  24096  tsmsres  24173  trust  24259  restutopopn  24268  metrest  24558  reperflem  24859  ellimc3  25934  limcflf  25936  lhop1lem  26072  ppinprm  27213  chtnprm  27215  chtppilimlem1  27535  orthin  31478  3oalem6  31699  mdslle1i  32349  mdslle2i  32350  mdslj1i  32351  mdslj2i  32352  mdslmd1lem2  32358  mdslmd3i  32364  mdexchi  32367  eulerpartlemn  34346  poimirlem3  37583  poimirlem29  37609  ismblfin  37621  nnuzdisj  45270  sumnnodd  45551  liminfgord  45675  sge0less  46313  sepnsepo  48603