Theorem ssrin 4208

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2109   ∩ cin 3916   ⊆ wss 3917

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 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-v 3452  df-in 3924  df-ss 3934

This theorem is referenced by:  sslin  4209  ssrind  4210  ss2in  4211  ssdisj  4426  ssdifin0  4452  ssres  5977  predpredss  6284  sbthlem7  9063  onsdominel  9096  infdifsn  9617  fin23lem23  10286  ttukeylem2  10470  limsupgord  15445  pjfval  21622  pjpm  21624  tgss  22862  neindisj2  23017  1stcrest  23347  kgencn3  23452  trfbas2  23737  fclsrest  23918  fcfnei  23929  cnextcn  23961  tsmsres  24038  trust  24124  restutopopn  24133  metrest  24419  reperflem  24714  ellimc3  25787  limcflf  25789  lhop1lem  25925  ppinprm  27069  chtnprm  27071  chtppilimlem1  27391  orthin  31382  3oalem6  31603  mdslle1i  32253  mdslle2i  32254  mdslj1i  32255  mdslj2i  32256  mdslmd1lem2  32262  mdslmd3i  32268  mdexchi  32271  eulerpartlemn  34379  poimirlem3  37624  poimirlem29  37650  ismblfin  37662  nnuzdisj  45358  sumnnodd  45635  liminfgord  45759  sge0less  46397  sepnsepo  48916