Theorem ssrin 4187

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

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

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 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3453  df-in 3906  df-ss 3916

This theorem is used by:  sslin  4188  ssrind  4189  ss2in  4190  ssinss1  4191  ssdisj  4413  ssdifin0  4441  ssres  5994  predpredss  6304  sbthlem7  9096  onsdominel  9129  infdifsn  9642  fin23lem23  10385  ttukeylem2  10569  limsupgord  15619  pjfval  21992  pjpm  21994  tgss  23266  neindisj2  23421  1stcrest  23751  kgencn3  23857  trfbas2  24142  fclsrest  24323  fcfnei  24334  cnextcn  24366  tsmsres  24443  trust  24528  restutopopn  24537  metrest  24823  reperflem  25118  ellimc3  26179  limcflf  26181  lhop1lem  26313  ppinprm  27461  chtnprm  27463  chtppilimlem1  27782  orthin  32030  3oalem6  32251  mdslle1i  32901  mdslle2i  32902  mdslj1i  32903  mdslj2i  32904  mdslmd1lem2  32910  mdslmd3i  32916  mdexchi  32919  eulerpartlemn  34996  dfttc4  37288  poimirlem3  38509  poimirlem29  38535  ismblfin  38547  nnuzdisj  46311  sumnnodd  46586  liminfgord  46708  sge0less  47346  sepnsepo  49976