Theorem ssrin 4192

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2111   ∩ cin 3901   ⊆ wss 3902

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-v 3438  df-in 3909  df-ss 3919

This theorem is referenced by:  sslin  4193  ssrind  4194  ss2in  4195  ssdisj  4410  ssdifin0  4436  ssres  5952  predpredss  6255  sbthlem7  9006  onsdominel  9039  infdifsn  9547  fin23lem23  10214  ttukeylem2  10398  limsupgord  15376  pjfval  21641  pjpm  21643  tgss  22881  neindisj2  23036  1stcrest  23366  kgencn3  23471  trfbas2  23756  fclsrest  23937  fcfnei  23948  cnextcn  23980  tsmsres  24057  trust  24142  restutopopn  24151  metrest  24437  reperflem  24732  ellimc3  25805  limcflf  25807  lhop1lem  25943  ppinprm  27087  chtnprm  27089  chtppilimlem1  27409  orthin  31421  3oalem6  31642  mdslle1i  32292  mdslle2i  32293  mdslj1i  32294  mdslj2i  32295  mdslmd1lem2  32301  mdslmd3i  32307  mdexchi  32310  eulerpartlemn  34389  poimirlem3  37662  poimirlem29  37688  ismblfin  37700  nnuzdisj  45393  sumnnodd  45669  liminfgord  45791  sge0less  46429  sepnsepo  48954