Theorem ssrin 4195

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 3932	. . . 4 ⊢ (𝐴 ⊆ 𝐵 → (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
2	1	anim1d 622	. . 3 ⊢ (𝐴 ⊆ 𝐵 → ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐶) → (𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶)))
3		elin 3922	. . 3 ⊢ (𝑥 ∈ (𝐴 ∩ 𝐶) ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐶))
4		elin 3922	. . 3 ⊢ (𝑥 ∈ (𝐵 ∩ 𝐶) ↔ (𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶))
5	2, 3, 4	3imtr4g 299	. 2 ⊢ (𝐴 ⊆ 𝐵 → (𝑥 ∈ (𝐴 ∩ 𝐶) → 𝑥 ∈ (𝐵 ∩ 𝐶)))
6	5	ssrdv 3944	1 ⊢ (𝐴 ⊆ 𝐵 → (𝐴 ∩ 𝐶) ⊆ (𝐵 ∩ 𝐶))

Syntax hints:   → wi 4   ∧ wa 400   ∈ wcel 2143   ∩ cin 3905   ⊆ wss 3906

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-v 3457  df-in 3913  df-ss 3923

This theorem is referenced by:  sslin  4196  ssrind  4197  ss2in  4198  ssinss1  4199  ssdisj  4421  ssdifin0  4447  ssres  6004  predpredss  6311  sbthlem7  9082  onsdominel  9115  infdifsn  9627  fin23lem23  10311  ttukeylem2  10495  limsupgord  15525  pjfval  21837  pjpm  21839  tgss  23106  neindisj2  23261  1stcrest  23591  kgencn3  23696  trfbas2  23981  fclsrest  24162  fcfnei  24173  cnextcn  24205  tsmsres  24282  trust  24367  restutopopn  24376  metrest  24662  reperflem  24957  ellimc3  26019  limcflf  26021  lhop1lem  26153  ppinprm  27294  chtnprm  27296  chtppilimlem1  27615  orthin  31776  3oalem6  31997  mdslle1i  32647  mdslle2i  32648  mdslj1i  32649  mdslj2i  32650  mdslmd1lem2  32656  mdslmd3i  32662  mdexchi  32665  eulerpartlemn  34749  dfttc4  37019  poimirlem3  38252  poimirlem29  38278  ismblfin  38290  nnuzdisj  46051  sumnnodd  46326  liminfgord  46448  sge0less  47086  sepnsepo  49679