Theorem ssrin 3871

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

Syntax hints:   → wi 4   ∧ wa 383   ∈ wcel 2030   ∩ cin 3606   ⊆ wss 3607

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-v 3233  df-in 3614  df-ss 3621

This theorem is referenced by:  sslin  3872  ss2in  3873  ssdisj  4059  ssdisjOLD  4060  ssdifin0  4083  ssres  5459  predpredss  5724  sbthlem7  8117  onsdominel  8150  phplem2  8181  infdifsn  8592  fictb  9105  fin23lem23  9186  ttukeylem2  9370  limsupgord  14247  xpsc1  16268  isacs1i  16365  rescabs  16540  lsmdisj  18140  dmdprdsplit2lem  18490  pjfval  20098  pjpm  20100  obselocv  20120  tgss  20820  neindisj2  20975  restbas  21010  neitr  21032  restcls  21033  restntr  21034  nrmsep  21209  1stcrest  21304  cldllycmp  21346  kgencn3  21409  trfbas2  21694  fclsneii  21868  fclsrest  21875  fcfnei  21886  cnextcn  21918  tsmsres  21994  trust  22080  restutopopn  22089  trcfilu  22145  metrest  22376  reperflem  22668  metdseq0  22704  iundisj2  23363  uniioombllem3  23399  ellimc3  23688  limcflf  23690  lhop1lem  23821  ppisval  24875  ppisval2  24876  ppinprm  24923  chtnprm  24925  chtwordi  24927  ppiwordi  24933  chpub  24990  chebbnd1lem1  25203  chtppilimlem1  25207  orthin  28433  3oalem6  28654  mdbr2  29283  mdslle1i  29304  mdslle2i  29305  mdslj1i  29306  mdslj2i  29307  mdsl2i  29309  mdslmd1lem1  29312  mdslmd1lem2  29313  mdslmd3i  29319  mdexchi  29322  sumdmdlem  29405  iundisj2f  29529  iundisj2fi  29684  esumrnmpt2  30258  eulerpartlemn  30571  bnj1177  31200  poimirlem3  33542  poimirlem29  33568  ismblfin  33580  sstotbnd2  33703  lcvexchlem5  34643  pnonsingN  35537  dochnoncon  36997  eldioph2lem2  37641  acsfn1p  38086  ssrind  39647  nnuzdisj  39884  sumnnodd  40180  limsupres  40255  liminfgord  40304  sge0less  40927  rhmsscrnghm  42351  rngcresringcat  42355