Theorem ssrin 4242

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 3977	. . . 4 ⊢ (𝐴 ⊆ 𝐵 → (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
2	1	anim1d 611	. . 3 ⊢ (𝐴 ⊆ 𝐵 → ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐶) → (𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶)))
3		elin 3967	. . 3 ⊢ (𝑥 ∈ (𝐴 ∩ 𝐶) ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐶))
4		elin 3967	. . 3 ⊢ (𝑥 ∈ (𝐵 ∩ 𝐶) ↔ (𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶))
5	2, 3, 4	3imtr4g 296	. 2 ⊢ (𝐴 ⊆ 𝐵 → (𝑥 ∈ (𝐴 ∩ 𝐶) → 𝑥 ∈ (𝐵 ∩ 𝐶)))
6	5	ssrdv 3989	1 ⊢ (𝐴 ⊆ 𝐵 → (𝐴 ∩ 𝐶) ⊆ (𝐵 ∩ 𝐶))

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2108   ∩ cin 3950   ⊆ wss 3951

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3482  df-in 3958  df-ss 3968

This theorem is referenced by:  sslin  4243  ssrind  4244  ss2in  4245  ssdisj  4460  ssdifin0  4486  ssres  6021  predpredss  6328  sbthlem7  9129  onsdominel  9166  phplem2OLD  9255  infdifsn  9697  fin23lem23  10366  ttukeylem2  10550  limsupgord  15508  pjfval  21726  pjpm  21728  tgss  22975  neindisj2  23131  1stcrest  23461  kgencn3  23566  trfbas2  23851  fclsrest  24032  fcfnei  24043  cnextcn  24075  tsmsres  24152  trust  24238  restutopopn  24247  metrest  24537  reperflem  24840  ellimc3  25914  limcflf  25916  lhop1lem  26052  ppinprm  27195  chtnprm  27197  chtppilimlem1  27517  orthin  31465  3oalem6  31686  mdslle1i  32336  mdslle2i  32337  mdslj1i  32338  mdslj2i  32339  mdslmd1lem2  32345  mdslmd3i  32351  mdexchi  32354  eulerpartlemn  34383  poimirlem3  37630  poimirlem29  37656  ismblfin  37668  nnuzdisj  45366  sumnnodd  45645  liminfgord  45769  sge0less  46407  sepnsepo  48821