Theorem ssrin 3981

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

Syntax hints:   → wi 4   ∧ wa 383   ∈ wcel 2139   ∩ cin 3714   ⊆ wss 3715

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-v 3342  df-in 3722  df-ss 3729

This theorem is referenced by:  sslin  3982  ss2in  3983  ssdisj  4170  ssdisjOLD  4171  ssdifin0  4194  ssres  5582  predpredss  5847  sbthlem7  8241  onsdominel  8274  phplem2  8305  infdifsn  8727  fictb  9259  fin23lem23  9340  ttukeylem2  9524  limsupgord  14402  xpsc1  16423  isacs1i  16519  rescabs  16694  lsmdisj  18294  dmdprdsplit2lem  18644  pjfval  20252  pjpm  20254  obselocv  20274  tgss  20974  neindisj2  21129  restbas  21164  neitr  21186  restcls  21187  restntr  21188  nrmsep  21363  1stcrest  21458  cldllycmp  21500  kgencn3  21563  trfbas2  21848  fclsneii  22022  fclsrest  22029  fcfnei  22040  cnextcn  22072  tsmsres  22148  trust  22234  restutopopn  22243  trcfilu  22299  metrest  22530  reperflem  22822  metdseq0  22858  iundisj2  23517  uniioombllem3  23553  ellimc3  23842  limcflf  23844  lhop1lem  23975  ppisval  25029  ppisval2  25030  ppinprm  25077  chtnprm  25079  chtwordi  25081  ppiwordi  25087  chpub  25144  chebbnd1lem1  25357  chtppilimlem1  25361  orthin  28614  3oalem6  28835  mdbr2  29464  mdslle1i  29485  mdslle2i  29486  mdslj1i  29487  mdslj2i  29488  mdsl2i  29490  mdslmd1lem1  29493  mdslmd1lem2  29494  mdslmd3i  29500  mdexchi  29503  sumdmdlem  29586  iundisj2f  29710  iundisj2fi  29865  esumrnmpt2  30439  eulerpartlemn  30752  bnj1177  31381  poimirlem3  33725  poimirlem29  33751  ismblfin  33763  sstotbnd2  33886  lcvexchlem5  34828  pnonsingN  35722  dochnoncon  37182  eldioph2lem2  37826  acsfn1p  38271  ssrind  39832  nnuzdisj  40069  sumnnodd  40365  limsupres  40440  liminfgord  40489  sge0less  41112  rhmsscrnghm  42536  rngcresringcat  42540