Theorem ssrin 3526

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	|- ( A C_ B -> ( A i^i C ) C_ ( B i^i C ) )

Proof of Theorem ssrin

Dummy variable x is distinct from all other variables.

Step	Hyp	Ref	Expression
1		ssel 3302	. . . 4 |- ( A C_ B -> ( x e. A -> x e. B ) )
2	1	anim1d 548	. . 3 |- ( A C_ B -> ( ( x e. A /\ x e. C ) -> ( x e. B /\ x e. C ) ) )
3		elin 3490	. . 3 |- ( x e. ( A i^i C ) <-> ( x e. A /\ x e. C ) )
4		elin 3490	. . 3 |- ( x e. ( B i^i C ) <-> ( x e. B /\ x e. C ) )
5	2, 3, 4	3imtr4g 262	. 2 |- ( A C_ B -> ( x e. ( A i^i C ) -> x e. ( B i^i C ) ) )
6	5	ssrdv 3314	1 |- ( A C_ B -> ( A i^i C ) C_ ( B i^i C ) )

Syntax hints:   -> wi 4   /\ wa 359   e. wcel 1721   i^i cin 3279   C_ wss 3280

This theorem is referenced by:  sslin  3527  ss2in  3528  ssdisj  3637  ssdifin0  3669  ssres  5131  sbthlem7  7182  onsdominel  7215  phplem2  7246  infdifsn  7567  fictb  8081  fin23lem23  8162  ttukeylem2  8346  limsupgord  12221  xpsc1  13741  isacs1i  13837  rescabs  13988  lsmdisj  15268  dmdprdsplit2lem  15558  pjfval  16888  pjpm  16890  obselocv  16910  tgss  16988  neindisj2  17142  restbas  17176  neitr  17198  restcls  17199  restntr  17200  nrmsep  17375  1stcrest  17469  cldllycmp  17511  kgencn3  17543  trfbas2  17828  fclsneii  18002  fclsrest  18009  fcfnei  18020  cnextcn  18051  tsmsres  18126  trust  18212  restutopopn  18221  trcfilu  18277  metrest  18507  reperflem  18802  metdseq0  18837  iundisj2  19396  uniioombllem3  19430  ellimc3  19719  limcflf  19721  lhop1lem  19850  ppisval  20839  ppisval2  20840  ppinprm  20888  chtnprm  20890  chtwordi  20892  ppiwordi  20898  chpub  20957  chebbnd1lem1  21116  chtppilimlem1  21120  orthin  22901  3oalem6  23122  mdbr2  23752  mdslle1i  23773  mdslle2i  23774  mdslj1i  23775  mdslj2i  23776  mdsl2i  23778  mdslmd1lem1  23781  mdslmd1lem2  23782  mdslmd3i  23788  mdexchi  23791  sumdmdlem  23874  iundisj2f  23983  iundisj2fi  24106  predpredss  25386  ismblfin  26146  sstotbnd2  26373  eldioph2lem2  26709  acsfn1p  27375  bnj1177  29081  lcvexchlem5  29521  pnonsingN  30415  dochnoncon  31874

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385

This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-v 2918  df-in 3287  df-ss 3294