Theorem ssrin 4182

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

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

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3431  df-in 3896  df-ss 3906

This theorem is referenced by:  sslin  4183  ssrind  4184  ss2in  4185  ssdisj  4400  ssdifin0  4425  ssres  5968  predpredss  6272  sbthlem7  9031  onsdominel  9064  infdifsn  9578  fin23lem23  10248  ttukeylem2  10432  limsupgord  15434  pjfval  21686  pjpm  21688  tgss  22933  neindisj2  23088  1stcrest  23418  kgencn3  23523  trfbas2  23808  fclsrest  23989  fcfnei  24000  cnextcn  24032  tsmsres  24109  trust  24194  restutopopn  24203  metrest  24489  reperflem  24784  ellimc3  25846  limcflf  25848  lhop1lem  25980  ppinprm  27115  chtnprm  27117  chtppilimlem1  27436  orthin  31517  3oalem6  31738  mdslle1i  32388  mdslle2i  32389  mdslj1i  32390  mdslj2i  32391  mdslmd1lem2  32397  mdslmd3i  32403  mdexchi  32406  eulerpartlemn  34525  dfttc4  36712  poimirlem3  37944  poimirlem29  37970  ismblfin  37982  nnuzdisj  45785  sumnnodd  46060  liminfgord  46182  sge0less  46820  sepnsepo  49399