Theorem ssrin 4141

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∈ wcel 2147   ⊆ wss 3900   ∩ cin 4092

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-v 3456  df-ss 3901  df-in 4094

This theorem is used by:  sslin  4142  ssrind  4143  ss2in  4144  ssinss1  4145  ssdisj  4416  ssdifin0  4444  ssres  6006  predpredss  6332  sbthlem7  9143  onsdominel  9176  infdifsn  9688  fin23lem23  10434  ttukeylem2  10618  limsupgord  15671  pjfval  22045  pjpm  22047  tgss  23319  neindisj2  23474  1stcrest  23804  kgencn3  23910  trfbas2  24195  fclsrest  24376  fcfnei  24387  cnextcn  24419  tsmsres  24496  trust  24581  restutopopn  24590  metrest  24876  reperflem  25171  ellimc3  26232  limcflf  26234  lhop1lem  26366  ppinprm  27512  chtnprm  27514  chtppilimlem1  27833  orthin  32081  3oalem6  32302  mdslle1i  32952  mdslle2i  32953  mdslj1i  32954  mdslj2i  32955  mdslmd1lem2  32961  mdslmd3i  32967  mdexchi  32970  eulerpartlemn  35096  dfttc4  37509  poimirlem3  38746  poimirlem29  38772  ismblfin  38784  nnuzdisj  46582  sumnnodd  46857  liminfgord  46979  sge0less  47617  sepnsepo  50253