Theorem ssrin 4191

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2113   ∩ cin 3897   ⊆ wss 3898

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 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-v 3439  df-in 3905  df-ss 3915

This theorem is referenced by:  sslin  4192  ssrind  4193  ss2in  4194  ssdisj  4409  ssdifin0  4435  ssres  5956  predpredss  6260  sbthlem7  9013  onsdominel  9046  infdifsn  9554  fin23lem23  10224  ttukeylem2  10408  limsupgord  15381  pjfval  21645  pjpm  21647  tgss  22884  neindisj2  23039  1stcrest  23369  kgencn3  23474  trfbas2  23759  fclsrest  23940  fcfnei  23951  cnextcn  23983  tsmsres  24060  trust  24145  restutopopn  24154  metrest  24440  reperflem  24735  ellimc3  25808  limcflf  25810  lhop1lem  25946  ppinprm  27090  chtnprm  27092  chtppilimlem1  27412  orthin  31428  3oalem6  31649  mdslle1i  32299  mdslle2i  32300  mdslj1i  32301  mdslj2i  32302  mdslmd1lem2  32308  mdslmd3i  32314  mdexchi  32317  eulerpartlemn  34415  poimirlem3  37683  poimirlem29  37709  ismblfin  37721  nnuzdisj  45478  sumnnodd  45754  liminfgord  45876  sge0less  46514  sepnsepo  49048