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

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

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 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3440  df-in 3912  df-ss 3922

This theorem is referenced by:  sslin  4196  ssrind  4197  ss2in  4198  ssdisj  4413  ssdifin0  4439  ssres  5958  predpredss  6260  sbthlem7  9017  onsdominel  9050  infdifsn  9572  fin23lem23  10239  ttukeylem2  10423  limsupgord  15397  pjfval  21631  pjpm  21633  tgss  22871  neindisj2  23026  1stcrest  23356  kgencn3  23461  trfbas2  23746  fclsrest  23927  fcfnei  23938  cnextcn  23970  tsmsres  24047  trust  24133  restutopopn  24142  metrest  24428  reperflem  24723  ellimc3  25796  limcflf  25798  lhop1lem  25934  ppinprm  27078  chtnprm  27080  chtppilimlem1  27400  orthin  31408  3oalem6  31629  mdslle1i  32279  mdslle2i  32280  mdslj1i  32281  mdslj2i  32282  mdslmd1lem2  32288  mdslmd3i  32294  mdexchi  32297  eulerpartlemn  34348  poimirlem3  37602  poimirlem29  37628  ismblfin  37640  nnuzdisj  45335  sumnnodd  45612  liminfgord  45736  sge0less  46374  sepnsepo  48909