Theorem ssrin 3708

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 3483	. . . 4 |- ( A C_ B -> ( x e. A -> x e. B ) )
2	1	anim1d 564	. . 3 |- ( A C_ B -> ( ( x e. A /\ x e. C ) -> ( x e. B /\ x e. C ) ) )
3		elin 3672	. . 3 |- ( x e. ( A i^i C ) <-> ( x e. A /\ x e. C ) )
4		elin 3672	. . 3 |- ( x e. ( B i^i C ) <-> ( x e. B /\ x e. C ) )
5	2, 3, 4	3imtr4g 270	. 2 |- ( A C_ B -> ( x e. ( A i^i C ) -> x e. ( B i^i C ) ) )
6	5	ssrdv 3495	1 |- ( A C_ B -> ( A i^i C ) C_ ( B i^i C ) )

Syntax hints:   -> wi 4   /\ wa 369   e. wcel 1804   i^i cin 3460   C_ wss 3461

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-v 3097  df-in 3468  df-ss 3475

This theorem is referenced by:  sslin  3709  ss2in  3710  ssdisj  3862  ssdifin0  3895  ssres  5289  sbthlem7  7635  onsdominel  7668  phplem2  7699  infdifsn  8076  fictb  8628  fin23lem23  8709  ttukeylem2  8893  limsupgord  13274  xpsc1  14835  isacs1i  14931  rescabs  15079  lsmdisj  16573  dmdprdsplit2lem  16968  pjfval  18610  pjpm  18612  obselocv  18632  tgss  19343  neindisj2  19497  restbas  19532  neitr  19554  restcls  19555  restntr  19556  nrmsep  19731  1stcrest  19827  cldllycmp  19869  kgencn3  19932  trfbas2  20217  fclsneii  20391  fclsrest  20398  fcfnei  20409  cnextcn  20440  tsmsresOLD  20518  tsmsres  20519  trust  20605  restutopopn  20614  trcfilu  20670  metrest  20900  reperflem  21196  metdseq0  21231  iundisj2  21832  uniioombllem3  21867  ellimc3  22156  limcflf  22158  lhop1lem  22287  ppisval  23249  ppisval2  23250  ppinprm  23298  chtnprm  23300  chtwordi  23302  ppiwordi  23308  chpub  23367  chebbnd1lem1  23526  chtppilimlem1  23530  orthin  26236  3oalem6  26457  mdbr2  27087  mdslle1i  27108  mdslle2i  27109  mdslj1i  27110  mdslj2i  27111  mdsl2i  27113  mdslmd1lem1  27116  mdslmd1lem2  27117  mdslmd3i  27123  mdexchi  27126  sumdmdlem  27209  iundisj2f  27321  iundisj2fi  27474  eulerpartlemn  28193  predpredss  29225  ismblfin  30030  sstotbnd2  30245  eldioph2lem2  30669  acsfn1p  31124  sumnnodd  31544  rhmsscrnghm  32571  rngcresringcat  32575  bnj1177  33795  lcvexchlem5  34503  pnonsingN  35397  dochnoncon  36858