Theorem ssrin 4183

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2114   ∩ cin 3889   ⊆ wss 3890

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3432  df-in 3897  df-ss 3907

This theorem is referenced by:  sslin  4184  ssrind  4185  ss2in  4186  ssdisj  4401  ssdifin0  4426  ssres  5962  predpredss  6266  sbthlem7  9024  onsdominel  9057  infdifsn  9569  fin23lem23  10239  ttukeylem2  10423  limsupgord  15425  pjfval  21696  pjpm  21698  tgss  22943  neindisj2  23098  1stcrest  23428  kgencn3  23533  trfbas2  23818  fclsrest  23999  fcfnei  24010  cnextcn  24042  tsmsres  24119  trust  24204  restutopopn  24213  metrest  24499  reperflem  24794  ellimc3  25856  limcflf  25858  lhop1lem  25990  ppinprm  27129  chtnprm  27131  chtppilimlem1  27450  orthin  31532  3oalem6  31753  mdslle1i  32403  mdslle2i  32404  mdslj1i  32405  mdslj2i  32406  mdslmd1lem2  32412  mdslmd3i  32418  mdexchi  32421  eulerpartlemn  34541  dfttc4  36728  poimirlem3  37958  poimirlem29  37984  ismblfin  37996  nnuzdisj  45803  sumnnodd  46078  liminfgord  46200  sge0less  46838  sepnsepo  49411