Theorem ssrin 4234

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

Syntax hints:   → wi 4   ∧ wa 397   ∈ wcel 2107   ∩ cin 3948   ⊆ wss 3949

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-in 3956  df-ss 3966

This theorem is referenced by:  sslin  4235  ssrind  4236  ss2in  4237  ssdisj  4460  ssdifin0  4486  ssres  6009  predpredss  6308  sbthlem7  9089  onsdominel  9126  phplem2OLD  9218  infdifsn  9652  fin23lem23  10321  ttukeylem2  10505  limsupgord  15416  pjfval  21261  pjpm  21263  tgss  22471  neindisj2  22627  1stcrest  22957  kgencn3  23062  trfbas2  23347  fclsrest  23528  fcfnei  23539  cnextcn  23571  tsmsres  23648  trust  23734  restutopopn  23743  metrest  24033  reperflem  24334  ellimc3  25396  limcflf  25398  lhop1lem  25530  ppinprm  26656  chtnprm  26658  chtppilimlem1  26976  orthin  30699  3oalem6  30920  mdslle1i  31570  mdslle2i  31571  mdslj1i  31572  mdslj2i  31573  mdslmd1lem2  31579  mdslmd3i  31585  mdexchi  31588  eulerpartlemn  33380  poimirlem3  36491  poimirlem29  36517  ismblfin  36529  nnuzdisj  44065  sumnnodd  44346  liminfgord  44470  sge0less  45108  sepnsepo  47556