Theorem ssrin 4196

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3444  df-in 3910  df-ss 3920

This theorem is referenced by:  sslin  4197  ssrind  4198  ss2in  4199  ssdisj  4414  ssdifin0  4440  ssres  5970  predpredss  6274  sbthlem7  9033  onsdominel  9066  infdifsn  9578  fin23lem23  10248  ttukeylem2  10432  limsupgord  15407  pjfval  21673  pjpm  21675  tgss  22924  neindisj2  23079  1stcrest  23409  kgencn3  23514  trfbas2  23799  fclsrest  23980  fcfnei  23991  cnextcn  24023  tsmsres  24100  trust  24185  restutopopn  24194  metrest  24480  reperflem  24775  ellimc3  25848  limcflf  25850  lhop1lem  25986  ppinprm  27130  chtnprm  27132  chtppilimlem1  27452  orthin  31533  3oalem6  31754  mdslle1i  32404  mdslle2i  32405  mdslj1i  32406  mdslj2i  32407  mdslmd1lem2  32413  mdslmd3i  32419  mdexchi  32422  eulerpartlemn  34558  poimirlem3  37868  poimirlem29  37894  ismblfin  37906  nnuzdisj  45708  sumnnodd  45984  liminfgord  46106  sge0less  46744  sepnsepo  49277