Theorem ssrin 4196

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

Syntax hints:   → wi 4   ∧ wa 400   ∈ wcel 2145   ∩ cin 3906   ⊆ wss 3907

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1566  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-v 3459  df-in 3914  df-ss 3924

This theorem is referenced by:  sslin  4197  ssrind  4198  ss2in  4199  ssinss1  4200  ssdisj  4417  ssdifin0  4442  ssres  5993  predpredss  6299  sbthlem7  9069  onsdominel  9102  infdifsn  9614  fin23lem23  10298  ttukeylem2  10482  limsupgord  15513  pjfval  21816  pjpm  21818  tgss  23086  neindisj2  23241  1stcrest  23571  kgencn3  23676  trfbas2  23961  fclsrest  24142  fcfnei  24153  cnextcn  24185  tsmsres  24262  trust  24347  restutopopn  24356  metrest  24642  reperflem  24937  ellimc3  25999  limcflf  26001  lhop1lem  26133  ppinprm  27274  chtnprm  27276  chtppilimlem1  27595  orthin  31707  3oalem6  31928  mdslle1i  32578  mdslle2i  32579  mdslj1i  32580  mdslj2i  32581  mdslmd1lem2  32587  mdslmd3i  32593  mdexchi  32596  eulerpartlemn  34688  dfttc4  36903  poimirlem3  38134  poimirlem29  38160  ismblfin  38172  nnuzdisj  45929  sumnnodd  46204  liminfgord  46326  sge0less  46964  sepnsepo  49553