Theorem ssrin 4138

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∈ wcel 2144   ⊆ wss 3895   ∩ cin 4089

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-ss 3896  df-in 4091

This theorem is used by:  sslin  4139  ssrind  4140  ss2in  4141  ssinss1  4142  ssdisj  4412  ssdifin0  4440  ssres  5993  predpredss  6311  sbthlem7  9115  onsdominel  9148  infdifsn  9661  fin23lem23  10407  ttukeylem2  10591  limsupgord  15644  pjfval  22017  pjpm  22019  tgss  23291  neindisj2  23446  1stcrest  23776  kgencn3  23882  trfbas2  24167  fclsrest  24348  fcfnei  24359  cnextcn  24391  tsmsres  24468  trust  24553  restutopopn  24562  metrest  24848  reperflem  25143  ellimc3  26204  limcflf  26206  lhop1lem  26338  ppinprm  27484  chtnprm  27486  chtppilimlem1  27805  orthin  32053  3oalem6  32274  mdslle1i  32924  mdslle2i  32925  mdslj1i  32926  mdslj2i  32927  mdslmd1lem2  32933  mdslmd3i  32939  mdexchi  32942  eulerpartlemn  35059  dfttc4  37410  poimirlem3  38634  poimirlem29  38660  ismblfin  38672  nnuzdisj  46460  sumnnodd  46735  liminfgord  46857  sge0less  47495  sepnsepo  50131