Theorem ssrin 3799

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 3561	. . . 4 ⊢ (𝐴 ⊆ 𝐵 → (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐵))
2	1	anim1d 585	. . 3 ⊢ (𝐴 ⊆ 𝐵 → ((𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐶) → (𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶)))
3		elin 3757	. . 3 ⊢ (𝑥 ∈ (𝐴 ∩ 𝐶) ↔ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐶))
4		elin 3757	. . 3 ⊢ (𝑥 ∈ (𝐵 ∩ 𝐶) ↔ (𝑥 ∈ 𝐵 ∧ 𝑥 ∈ 𝐶))
5	2, 3, 4	3imtr4g 283	. 2 ⊢ (𝐴 ⊆ 𝐵 → (𝑥 ∈ (𝐴 ∩ 𝐶) → 𝑥 ∈ (𝐵 ∩ 𝐶)))
6	5	ssrdv 3573	1 ⊢ (𝐴 ⊆ 𝐵 → (𝐴 ∩ 𝐶) ⊆ (𝐵 ∩ 𝐶))

Syntax hints:   → wi 4   ∧ wa 382   ∈ wcel 1976   ∩ cin 3538   ⊆ wss 3539

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589

This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-v 3174  df-in 3546  df-ss 3553

This theorem is referenced by:  sslin  3800  ss2in  3801  ssdisj  3977  ssdisjOLD  3978  ssdifin0  4001  ssres  5330  predpredss  5588  sbthlem7  7938  onsdominel  7971  phplem2  8002  infdifsn  8414  fictb  8927  fin23lem23  9008  ttukeylem2  9192  limsupgord  13999  xpsc1  15992  isacs1i  16089  rescabs  16264  lsmdisj  17865  dmdprdsplit2lem  18215  pjfval  19816  pjpm  19818  obselocv  19838  tgss  20530  neindisj2  20684  restbas  20719  neitr  20741  restcls  20742  restntr  20743  nrmsep  20918  1stcrest  21013  cldllycmp  21055  kgencn3  21118  trfbas2  21404  fclsneii  21578  fclsrest  21585  fcfnei  21596  cnextcn  21628  tsmsres  21704  trust  21790  restutopopn  21799  trcfilu  21855  metrest  22086  reperflem  22376  metdseq0  22412  iundisj2  23068  uniioombllem3  23103  ellimc3  23393  limcflf  23395  lhop1lem  23524  ppisval  24574  ppisval2  24575  ppinprm  24622  chtnprm  24624  chtwordi  24626  ppiwordi  24632  chpub  24689  chebbnd1lem1  24902  chtppilimlem1  24906  orthin  27482  3oalem6  27703  mdbr2  28332  mdslle1i  28353  mdslle2i  28354  mdslj1i  28355  mdslj2i  28356  mdsl2i  28358  mdslmd1lem1  28361  mdslmd1lem2  28362  mdslmd3i  28368  mdexchi  28371  sumdmdlem  28454  iundisj2f  28578  iundisj2fi  28736  esumrnmpt2  29250  eulerpartlemn  29563  bnj1177  30121  poimirlem3  32365  poimirlem29  32391  ismblfin  32403  sstotbnd2  32526  lcvexchlem5  33126  pnonsingN  34020  dochnoncon  35481  eldioph2lem2  36125  acsfn1p  36571  nnuzdisj  38295  sumnnodd  38480  sge0less  39068  rhmsscrnghm  41799  rngcresringcat  41803