Theorem ssrin 4194

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

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

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3442  df-in 3908  df-ss 3918

This theorem is referenced by:  sslin  4195  ssrind  4196  ss2in  4197  ssdisj  4412  ssdifin0  4438  ssres  5962  predpredss  6266  sbthlem7  9021  onsdominel  9054  infdifsn  9566  fin23lem23  10236  ttukeylem2  10420  limsupgord  15395  pjfval  21661  pjpm  21663  tgss  22912  neindisj2  23067  1stcrest  23397  kgencn3  23502  trfbas2  23787  fclsrest  23968  fcfnei  23979  cnextcn  24011  tsmsres  24088  trust  24173  restutopopn  24182  metrest  24468  reperflem  24763  ellimc3  25836  limcflf  25838  lhop1lem  25974  ppinprm  27118  chtnprm  27120  chtppilimlem1  27440  orthin  31521  3oalem6  31742  mdslle1i  32392  mdslle2i  32393  mdslj1i  32394  mdslj2i  32395  mdslmd1lem2  32401  mdslmd3i  32407  mdexchi  32410  eulerpartlemn  34538  poimirlem3  37820  poimirlem29  37846  ismblfin  37858  nnuzdisj  45596  sumnnodd  45872  liminfgord  45994  sge0less  46632  sepnsepo  49165