Theorem ssrin 4190

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∈ wcel 2145   ∩ cin 3901   ⊆ wss 3902

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-v 3455  df-in 3909  df-ss 3919

This theorem is used by:  sslin  4191  ssrind  4192  ss2in  4193  ssinss1  4194  ssdisj  4416  ssdifin0  4444  ssres  6000  predpredss  6310  sbthlem7  9094  onsdominel  9127  infdifsn  9639  fin23lem23  10331  ttukeylem2  10515  limsupgord  15561  pjfval  21923  pjpm  21925  tgss  23197  neindisj2  23352  1stcrest  23682  kgencn3  23788  trfbas2  24073  fclsrest  24254  fcfnei  24265  cnextcn  24297  tsmsres  24374  trust  24459  restutopopn  24468  metrest  24754  reperflem  25049  ellimc3  26111  limcflf  26113  lhop1lem  26245  ppinprm  27389  chtnprm  27391  chtppilimlem1  27710  orthin  31928  3oalem6  32149  mdslle1i  32799  mdslle2i  32800  mdslj1i  32801  mdslj2i  32802  mdslmd1lem2  32808  mdslmd3i  32814  mdexchi  32817  eulerpartlemn  34894  dfttc4  37151  poimirlem3  38374  poimirlem29  38400  ismblfin  38412  nnuzdisj  46187  sumnnodd  46462  liminfgord  46584  sge0less  47222  sepnsepo  49852