Theorem ssrin 4217

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

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

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 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-v 3461  df-in 3933  df-ss 3943

This theorem is referenced by:  sslin  4218  ssrind  4219  ss2in  4220  ssdisj  4435  ssdifin0  4461  ssres  5990  predpredss  6297  sbthlem7  9103  onsdominel  9140  phplem2OLD  9229  infdifsn  9671  fin23lem23  10340  ttukeylem2  10524  limsupgord  15488  pjfval  21666  pjpm  21668  tgss  22906  neindisj2  23061  1stcrest  23391  kgencn3  23496  trfbas2  23781  fclsrest  23962  fcfnei  23973  cnextcn  24005  tsmsres  24082  trust  24168  restutopopn  24177  metrest  24463  reperflem  24758  ellimc3  25832  limcflf  25834  lhop1lem  25970  ppinprm  27114  chtnprm  27116  chtppilimlem1  27436  orthin  31427  3oalem6  31648  mdslle1i  32298  mdslle2i  32299  mdslj1i  32300  mdslj2i  32301  mdslmd1lem2  32307  mdslmd3i  32313  mdexchi  32316  eulerpartlemn  34413  poimirlem3  37647  poimirlem29  37673  ismblfin  37685  nnuzdisj  45382  sumnnodd  45659  liminfgord  45783  sge0less  46421  sepnsepo  48898