Theorem ssrin 4177

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 3916	. . . 4 ⊢ (𝐴 ⊆ 𝐵 → (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
2	1	anim1d 617	. . 3 ⊢ (𝐴 ⊆ 𝐵 → ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐶) → (𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶)))
3		elin 3906	. . 3 ⊢ (𝑥 ∈ (𝐴 ∩ 𝐶) ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐶))
4		elin 3906	. . 3 ⊢ (𝑥 ∈ (𝐵 ∩ 𝐶) ↔ (𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶))
5	2, 3, 4	3imtr4g 297	. 2 ⊢ (𝐴 ⊆ 𝐵 → (𝑥 ∈ (𝐴 ∩ 𝐶) → 𝑥 ∈ (𝐵 ∩ 𝐶)))
6	5	ssrdv 3928	1 ⊢ (𝐴 ⊆ 𝐵 → (𝐴 ∩ 𝐶) ⊆ (𝐵 ∩ 𝐶))

Syntax hints:   → wi 4   ∧ wa 396   ∈ wcel 2119   ∩ cin 3889   ⊆ wss 3890

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-v 3434  df-in 3897  df-ss 3907

This theorem is referenced by:  sslin  4178  ssrind  4179  ss2in  4180  ssdisj  4395  ssdifin0  4420  ssres  5962  predpredss  6266  sbthlem7  9028  onsdominel  9061  infdifsn  9576  fin23lem23  10246  ttukeylem2  10430  limsupgord  15432  pjfval  21688  pjpm  21690  tgss  22958  neindisj2  23113  1stcrest  23443  kgencn3  23548  trfbas2  23833  fclsrest  24014  fcfnei  24025  cnextcn  24057  tsmsres  24134  trust  24219  restutopopn  24228  metrest  24514  reperflem  24809  ellimc3  25871  limcflf  25873  lhop1lem  26005  ppinprm  27140  chtnprm  27142  chtppilimlem1  27461  orthin  31542  3oalem6  31763  mdslle1i  32413  mdslle2i  32414  mdslj1i  32415  mdslj2i  32416  mdslmd1lem2  32422  mdslmd3i  32428  mdexchi  32431  eulerpartlemn  34572  dfttc4  36765  poimirlem3  37997  poimirlem29  38023  ismblfin  38035  nnuzdisj  45807  sumnnodd  46082  liminfgord  46204  sge0less  46842  sepnsepo  49421