Theorem ssrin 4136

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 3889	. . . 4 ⊢ (𝐴 ⊆ 𝐵 → (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
2	1	anim1d 610	. . 3 ⊢ (𝐴 ⊆ 𝐵 → ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐶) → (𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶)))
3		elin 4096	. . 3 ⊢ (𝑥 ∈ (𝐴 ∩ 𝐶) ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐶))
4		elin 4096	. . 3 ⊢ (𝑥 ∈ (𝐵 ∩ 𝐶) ↔ (𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶))
5	2, 3, 4	3imtr4g 297	. 2 ⊢ (𝐴 ⊆ 𝐵 → (𝑥 ∈ (𝐴 ∩ 𝐶) → 𝑥 ∈ (𝐵 ∩ 𝐶)))
6	5	ssrdv 3901	1 ⊢ (𝐴 ⊆ 𝐵 → (𝐴 ∩ 𝐶) ⊆ (𝐵 ∩ 𝐶))

Syntax hints:   → wi 4   ∧ wa 396   ∈ wcel 2083   ∩ cin 3864   ⊆ wss 3865

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1781  ax-4 1795  ax-5 1892  ax-6 1951  ax-7 1996  ax-8 2085  ax-9 2093  ax-10 2114  ax-11 2128  ax-12 2143  ax-ext 2771

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-tru 1528  df-ex 1766  df-nf 1770  df-sb 2045  df-clab 2778  df-cleq 2790  df-clel 2865  df-nfc 2937  df-v 3442  df-in 3872  df-ss 3880

This theorem is referenced by:  sslin  4137  ssrind  4138  ss2in  4139  ssdisj  4329  ssdifin0  4351  ssres  5768  predpredss  6036  sbthlem7  8487  onsdominel  8520  phplem2  8551  infdifsn  8973  fin23lem23  9601  ttukeylem2  9785  limsupgord  14667  pjfval  20536  pjpm  20538  tgss  21264  neindisj2  21419  1stcrest  21749  kgencn3  21854  trfbas2  22139  fclsrest  22320  fcfnei  22331  cnextcn  22363  tsmsres  22439  trust  22525  restutopopn  22534  metrest  22821  reperflem  23113  ellimc3  24164  limcflf  24166  lhop1lem  24297  ppinprm  25415  chtnprm  25417  chtppilimlem1  25735  orthin  28910  3oalem6  29131  mdslle1i  29781  mdslle2i  29782  mdslj1i  29783  mdslj2i  29784  mdslmd1lem2  29790  mdslmd3i  29796  mdexchi  29799  eulerpartlemn  31252  poimirlem3  34447  poimirlem29  34473  ismblfin  34485  nnuzdisj  41185  sumnnodd  41474  liminfgord  41598  sge0less  42238