Theorem ssrin 4210

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

Syntax hints:   → wi 4   ∧ wa 398   ∈ wcel 2114   ∩ cin 3935   ⊆ wss 3936

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 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-v 3496  df-in 3943  df-ss 3952

This theorem is referenced by:  sslin  4211  ssrind  4212  ss2in  4213  ssdisj  4409  ssdifin0  4431  ssres  5880  predpredss  6154  sbthlem7  8633  onsdominel  8666  phplem2  8697  infdifsn  9120  fin23lem23  9748  ttukeylem2  9932  limsupgord  14829  pjfval  20850  pjpm  20852  tgss  21576  neindisj2  21731  1stcrest  22061  kgencn3  22166  trfbas2  22451  fclsrest  22632  fcfnei  22643  cnextcn  22675  tsmsres  22752  trust  22838  restutopopn  22847  metrest  23134  reperflem  23426  ellimc3  24477  limcflf  24479  lhop1lem  24610  ppinprm  25729  chtnprm  25731  chtppilimlem1  26049  orthin  29223  3oalem6  29444  mdslle1i  30094  mdslle2i  30095  mdslj1i  30096  mdslj2i  30097  mdslmd1lem2  30103  mdslmd3i  30109  mdexchi  30112  eulerpartlemn  31639  poimirlem3  34910  poimirlem29  34936  ismblfin  34948  nnuzdisj  41672  sumnnodd  41960  liminfgord  42084  sge0less  42723