Theorem ssrin 4249

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2105   ∩ cin 3961   ⊆ wss 3962

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1539  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-v 3479  df-in 3969  df-ss 3979

This theorem is referenced by:  sslin  4250  ssrind  4251  ss2in  4252  ssdisj  4465  ssdifin0  4491  ssres  6023  predpredss  6329  sbthlem7  9127  onsdominel  9164  phplem2OLD  9252  infdifsn  9694  fin23lem23  10363  ttukeylem2  10547  limsupgord  15504  pjfval  21743  pjpm  21745  tgss  22990  neindisj2  23146  1stcrest  23476  kgencn3  23581  trfbas2  23866  fclsrest  24047  fcfnei  24058  cnextcn  24090  tsmsres  24167  trust  24253  restutopopn  24262  metrest  24552  reperflem  24853  ellimc3  25928  limcflf  25930  lhop1lem  26066  ppinprm  27209  chtnprm  27211  chtppilimlem1  27531  orthin  31474  3oalem6  31695  mdslle1i  32345  mdslle2i  32346  mdslj1i  32347  mdslj2i  32348  mdslmd1lem2  32354  mdslmd3i  32360  mdexchi  32363  eulerpartlemn  34362  poimirlem3  37609  poimirlem29  37635  ismblfin  37647  nnuzdisj  45304  sumnnodd  45585  liminfgord  45709  sge0less  46347  sepnsepo  48719