Theorem ssrin 4164

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-in 3890  df-ss 3900

This theorem is referenced by:  sslin  4165  ssrind  4166  ss2in  4167  ssdisj  4390  ssdifin0  4413  ssres  5907  predpredss  6198  sbthlem7  8829  onsdominel  8862  phplem2  8893  infdifsn  9345  fin23lem23  10013  ttukeylem2  10197  limsupgord  15109  pjfval  20823  pjpm  20825  tgss  22026  neindisj2  22182  1stcrest  22512  kgencn3  22617  trfbas2  22902  fclsrest  23083  fcfnei  23094  cnextcn  23126  tsmsres  23203  trust  23289  restutopopn  23298  metrest  23586  reperflem  23887  ellimc3  24948  limcflf  24950  lhop1lem  25082  ppinprm  26206  chtnprm  26208  chtppilimlem1  26526  orthin  29709  3oalem6  29930  mdslle1i  30580  mdslle2i  30581  mdslj1i  30582  mdslj2i  30583  mdslmd1lem2  30589  mdslmd3i  30595  mdexchi  30598  eulerpartlemn  32248  poimirlem3  35707  poimirlem29  35733  ismblfin  35745  nnuzdisj  42784  sumnnodd  43061  liminfgord  43185  sge0less  43820  sepnsepo  46105