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  9095  onsdominel  9128  infdifsn  9640  fin23lem23  10332  ttukeylem2  10516  limsupgord  15563  pjfval  21925  pjpm  21927  tgss  23199  neindisj2  23354  1stcrest  23684  kgencn3  23790  trfbas2  24075  fclsrest  24256  fcfnei  24267  cnextcn  24299  tsmsres  24376  trust  24461  restutopopn  24470  metrest  24756  reperflem  25051  ellimc3  26113  limcflf  26115  lhop1lem  26247  ppinprm  27396  chtnprm  27398  chtppilimlem1  27717  orthin  31935  3oalem6  32156  mdslle1i  32806  mdslle2i  32807  mdslj1i  32808  mdslj2i  32809  mdslmd1lem2  32815  mdslmd3i  32821  mdexchi  32824  eulerpartlemn  34900  dfttc4  37157  poimirlem3  38380  poimirlem29  38406  ismblfin  38418  nnuzdisj  46193  sumnnodd  46468  liminfgord  46590  sge0less  47228  sepnsepo  49858