Theorem ssrin 3800

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 3562	. . . 4 ⊢ (𝐴 ⊆ 𝐵 → (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
2	1	anim1d 586	. . 3 ⊢ (𝐴 ⊆ 𝐵 → ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐶) → (𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶)))
3		elin 3758	. . 3 ⊢ (𝑥 ∈ (𝐴 ∩ 𝐶) ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐶))
4		elin 3758	. . 3 ⊢ (𝑥 ∈ (𝐵 ∩ 𝐶) ↔ (𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶))
5	2, 3, 4	3imtr4g 284	. 2 ⊢ (𝐴 ⊆ 𝐵 → (𝑥 ∈ (𝐴 ∩ 𝐶) → 𝑥 ∈ (𝐵 ∩ 𝐶)))
6	5	ssrdv 3574	1 ⊢ (𝐴 ⊆ 𝐵 → (𝐴 ∩ 𝐶) ⊆ (𝐵 ∩ 𝐶))

Syntax hints:   → wi 4   ∧ wa 383   ∈ wcel 1977   ∩ cin 3539   ⊆ wss 3540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-v 3175  df-in 3547  df-ss 3554

This theorem is referenced by:  sslin  3801  ss2in  3802  ssdisj  3978  ssdisjOLD  3979  ssdifin0  4002  ssres  5344  predpredss  5603  sbthlem7  7961  onsdominel  7994  phplem2  8025  infdifsn  8437  fictb  8950  fin23lem23  9031  ttukeylem2  9215  limsupgord  14051  xpsc1  16044  isacs1i  16141  rescabs  16316  lsmdisj  17917  dmdprdsplit2lem  18267  pjfval  19869  pjpm  19871  obselocv  19891  tgss  20583  neindisj2  20737  restbas  20772  neitr  20794  restcls  20795  restntr  20796  nrmsep  20971  1stcrest  21066  cldllycmp  21108  kgencn3  21171  trfbas2  21457  fclsneii  21631  fclsrest  21638  fcfnei  21649  cnextcn  21681  tsmsres  21757  trust  21843  restutopopn  21852  trcfilu  21908  metrest  22139  reperflem  22429  metdseq0  22465  iundisj2  23124  uniioombllem3  23159  ellimc3  23449  limcflf  23451  lhop1lem  23580  ppisval  24630  ppisval2  24631  ppinprm  24678  chtnprm  24680  chtwordi  24682  ppiwordi  24688  chpub  24745  chebbnd1lem1  24958  chtppilimlem1  24962  orthin  27689  3oalem6  27910  mdbr2  28539  mdslle1i  28560  mdslle2i  28561  mdslj1i  28562  mdslj2i  28563  mdsl2i  28565  mdslmd1lem1  28568  mdslmd1lem2  28569  mdslmd3i  28575  mdexchi  28578  sumdmdlem  28661  iundisj2f  28785  iundisj2fi  28943  esumrnmpt2  29457  eulerpartlemn  29770  bnj1177  30328  poimirlem3  32582  poimirlem29  32608  ismblfin  32620  sstotbnd2  32743  lcvexchlem5  33343  pnonsingN  34237  dochnoncon  35698  eldioph2lem2  36342  acsfn1p  36788  nnuzdisj  38512  sumnnodd  38697  sge0less  39285  rhmsscrnghm  41818  rngcresringcat  41822