Theorem ssrin 4197

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 3934	. . . 4 ⊢ (𝐴 ⊆ 𝐵 → (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
2	1	anim1d 623	. . 3 ⊢ (𝐴 ⊆ 𝐵 → ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐶) → (𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶)))
3		elin 3924	. . 3 ⊢ (𝑥 ∈ (𝐴 ∩ 𝐶) ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐶))
4		elin 3924	. . 3 ⊢ (𝑥 ∈ (𝐵 ∩ 𝐶) ↔ (𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶))
5	2, 3, 4	3imtr4g 299	. 2 ⊢ (𝐴 ⊆ 𝐵 → (𝑥 ∈ (𝐴 ∩ 𝐶) → 𝑥 ∈ (𝐵 ∩ 𝐶)))
6	5	ssrdv 3946	1 ⊢ (𝐴 ⊆ 𝐵 → (𝐴 ∩ 𝐶) ⊆ (𝐵 ∩ 𝐶))

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∈ wcel 2146   ∩ cin 3907   ⊆ wss 3908

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2738

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2745  df-cleq 2758  df-clel 2841  df-v 3460  df-in 3915  df-ss 3925

This theorem is used by:  sslin  4198  ssrind  4199  ss2in  4200  ssinss1  4201  ssdisj  4423  ssdifin0  4451  ssres  6007  predpredss  6316  sbthlem7  9091  onsdominel  9124  infdifsn  9636  fin23lem23  10328  ttukeylem2  10512  limsupgord  15549  pjfval  21893  pjpm  21895  tgss  23162  neindisj2  23317  1stcrest  23647  kgencn3  23752  trfbas2  24037  fclsrest  24218  fcfnei  24229  cnextcn  24261  tsmsres  24338  trust  24423  restutopopn  24432  metrest  24718  reperflem  25013  ellimc3  26075  limcflf  26077  lhop1lem  26209  ppinprm  27353  chtnprm  27355  chtppilimlem1  27674  orthin  31835  3oalem6  32056  mdslle1i  32706  mdslle2i  32707  mdslj1i  32708  mdslj2i  32709  mdslmd1lem2  32715  mdslmd3i  32721  mdexchi  32724  eulerpartlemn  34803  dfttc4  37082  poimirlem3  38315  poimirlem29  38341  ismblfin  38353  nnuzdisj  46112  sumnnodd  46387  liminfgord  46509  sge0less  47147  sepnsepo  49743