Theorem ssrin 4205

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

Syntax hints:   → wi 4   ∧ wa 395   ∈ wcel 2109   ∩ cin 3913   ⊆ wss 3914

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3449  df-in 3921  df-ss 3931

This theorem is referenced by:  sslin  4206  ssrind  4207  ss2in  4208  ssdisj  4423  ssdifin0  4449  ssres  5974  predpredss  6281  sbthlem7  9057  onsdominel  9090  infdifsn  9610  fin23lem23  10279  ttukeylem2  10463  limsupgord  15438  pjfval  21615  pjpm  21617  tgss  22855  neindisj2  23010  1stcrest  23340  kgencn3  23445  trfbas2  23730  fclsrest  23911  fcfnei  23922  cnextcn  23954  tsmsres  24031  trust  24117  restutopopn  24126  metrest  24412  reperflem  24707  ellimc3  25780  limcflf  25782  lhop1lem  25918  ppinprm  27062  chtnprm  27064  chtppilimlem1  27384  orthin  31375  3oalem6  31596  mdslle1i  32246  mdslle2i  32247  mdslj1i  32248  mdslj2i  32249  mdslmd1lem2  32255  mdslmd3i  32261  mdexchi  32264  eulerpartlemn  34372  poimirlem3  37617  poimirlem29  37643  ismblfin  37655  nnuzdisj  45351  sumnnodd  45628  liminfgord  45752  sge0less  46390  sepnsepo  48912