Theorem ssrin 3838

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 3597	. . . 4 ⊢ (𝐴 ⊆ 𝐵 → (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
2	1	anim1d 588	. . 3 ⊢ (𝐴 ⊆ 𝐵 → ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐶) → (𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶)))
3		elin 3796	. . 3 ⊢ (𝑥 ∈ (𝐴 ∩ 𝐶) ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐶))
4		elin 3796	. . 3 ⊢ (𝑥 ∈ (𝐵 ∩ 𝐶) ↔ (𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶))
5	2, 3, 4	3imtr4g 285	. 2 ⊢ (𝐴 ⊆ 𝐵 → (𝑥 ∈ (𝐴 ∩ 𝐶) → 𝑥 ∈ (𝐵 ∩ 𝐶)))
6	5	ssrdv 3609	1 ⊢ (𝐴 ⊆ 𝐵 → (𝐴 ∩ 𝐶) ⊆ (𝐵 ∩ 𝐶))

Syntax hints:   → wi 4   ∧ wa 384   ∈ wcel 1990   ∩ cin 3573   ⊆ wss 3574

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-v 3202  df-in 3581  df-ss 3588

This theorem is referenced by:  sslin  3839  ss2in  3840  ssdisj  4026  ssdisjOLD  4027  ssdifin0  4050  ssres  5424  predpredss  5686  sbthlem7  8076  onsdominel  8109  phplem2  8140  infdifsn  8554  fictb  9067  fin23lem23  9148  ttukeylem2  9332  limsupgord  14203  xpsc1  16221  isacs1i  16318  rescabs  16493  lsmdisj  18094  dmdprdsplit2lem  18444  pjfval  20050  pjpm  20052  obselocv  20072  tgss  20772  neindisj2  20927  restbas  20962  neitr  20984  restcls  20985  restntr  20986  nrmsep  21161  1stcrest  21256  cldllycmp  21298  kgencn3  21361  trfbas2  21647  fclsneii  21821  fclsrest  21828  fcfnei  21839  cnextcn  21871  tsmsres  21947  trust  22033  restutopopn  22042  trcfilu  22098  metrest  22329  reperflem  22621  metdseq0  22657  iundisj2  23317  uniioombllem3  23353  ellimc3  23643  limcflf  23645  lhop1lem  23776  ppisval  24830  ppisval2  24831  ppinprm  24878  chtnprm  24880  chtwordi  24882  ppiwordi  24888  chpub  24945  chebbnd1lem1  25158  chtppilimlem1  25162  orthin  28305  3oalem6  28526  mdbr2  29155  mdslle1i  29176  mdslle2i  29177  mdslj1i  29178  mdslj2i  29179  mdsl2i  29181  mdslmd1lem1  29184  mdslmd1lem2  29185  mdslmd3i  29191  mdexchi  29194  sumdmdlem  29277  iundisj2f  29403  iundisj2fi  29556  esumrnmpt2  30130  eulerpartlemn  30443  bnj1177  31074  poimirlem3  33412  poimirlem29  33438  ismblfin  33450  sstotbnd2  33573  lcvexchlem5  34325  pnonsingN  35219  dochnoncon  36680  eldioph2lem2  37324  acsfn1p  37769  ssrind  39333  nnuzdisj  39571  sumnnodd  39862  limsupres  39937  liminfgord  39986  sge0less  40609  rhmsscrnghm  42026  rngcresringcat  42030