Theorem ssrin 4193

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

Syntax hints:   → wi 4   ∧ wa 399   ∈ wcel 2141   ∩ cin 3903   ⊆ wss 3904

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1562  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3455  df-in 3911  df-ss 3921

This theorem is referenced by:  sslin  4194  ssrind  4195  ss2in  4196  ssinss1  4197  ssdisj  4413  ssdifin0  4438  ssres  5987  predpredss  6291  sbthlem7  9061  onsdominel  9094  infdifsn  9609  fin23lem23  10280  ttukeylem2  10464  limsupgord  15482  pjfval  21738  pjpm  21740  tgss  23008  neindisj2  23163  1stcrest  23493  kgencn3  23598  trfbas2  23883  fclsrest  24064  fcfnei  24075  cnextcn  24107  tsmsres  24184  trust  24269  restutopopn  24278  metrest  24564  reperflem  24859  ellimc3  25921  limcflf  25923  lhop1lem  26055  ppinprm  27193  chtnprm  27195  chtppilimlem1  27514  orthin  31595  3oalem6  31816  mdslle1i  32466  mdslle2i  32467  mdslj1i  32468  mdslj2i  32469  mdslmd1lem2  32475  mdslmd3i  32481  mdexchi  32484  eulerpartlemn  34639  dfttc4  36854  poimirlem3  38086  poimirlem29  38112  ismblfin  38124  nnuzdisj  45895  sumnnodd  46170  liminfgord  46292  sge0less  46930  sepnsepo  49509