Theorem ssrin 3668

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 3437	. . . 4 |- ( A C_ B -> ( x e. A -> x e. B ) )
2	1	anim1d 572	. . 3 |- ( A C_ B -> ( ( x e. A /\ x e. C ) -> ( x e. B /\ x e. C ) ) )
3		elin 3628	. . 3 |- ( x e. ( A i^i C ) <-> ( x e. A /\ x e. C ) )
4		elin 3628	. . 3 |- ( x e. ( B i^i C ) <-> ( x e. B /\ x e. C ) )
5	2, 3, 4	3imtr4g 278	. 2 |- ( A C_ B -> ( x e. ( A i^i C ) -> x e. ( B i^i C ) ) )
6	5	ssrdv 3449	1 |- ( A C_ B -> ( A i^i C ) C_ ( B i^i C ) )

Syntax hints:   -> wi 4   /\ wa 375   e. wcel 1897   i^i cin 3414   C_ wss 3415

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1679  ax-4 1692  ax-5 1768  ax-6 1815  ax-7 1861  ax-10 1925  ax-11 1930  ax-12 1943  ax-13 2101  ax-ext 2441

This theorem depends on definitions:  df-bi 190  df-an 377  df-tru 1457  df-ex 1674  df-nf 1678  df-sb 1808  df-clab 2448  df-cleq 2454  df-clel 2457  df-nfc 2591  df-v 3058  df-in 3422  df-ss 3429

This theorem is referenced by:  sslin  3669  ss2in  3670  ssdisj  3825  ssdifin0  3860  ssres  5148  predpredss  5404  sbthlem7  7713  onsdominel  7746  phplem2  7777  infdifsn  8187  fictb  8700  fin23lem23  8781  ttukeylem2  8965  limsupgord  13576  xpsc1  15515  isacs1i  15611  rescabs  15786  lsmdisj  17379  dmdprdsplit2lem  17726  pjfval  19317  pjpm  19319  obselocv  19339  tgss  20032  neindisj2  20187  restbas  20222  neitr  20244  restcls  20245  restntr  20246  nrmsep  20421  1stcrest  20516  cldllycmp  20558  kgencn3  20621  trfbas2  20906  fclsneii  21080  fclsrest  21087  fcfnei  21098  cnextcn  21130  tsmsres  21206  trust  21292  restutopopn  21301  trcfilu  21357  metrest  21587  reperflem  21884  metdseq0  21919  metdseq0OLD  21934  iundisj2  22550  uniioombllem3  22591  ellimc3  22882  limcflf  22884  lhop1lem  23013  ppisval  24078  ppisval2  24079  ppinprm  24127  chtnprm  24129  chtwordi  24131  ppiwordi  24137  chpub  24196  chebbnd1lem1  24355  chtppilimlem1  24359  orthin  27147  3oalem6  27368  mdbr2  27997  mdslle1i  28018  mdslle2i  28019  mdslj1i  28020  mdslj2i  28021  mdsl2i  28023  mdslmd1lem1  28026  mdslmd1lem2  28027  mdslmd3i  28033  mdexchi  28036  sumdmdlem  28119  iundisj2f  28248  iundisj2fi  28421  esumrnmpt2  28937  eulerpartlemn  29262  bnj1177  29863  poimirlem3  31987  poimirlem29  32013  ismblfin  32025  sstotbnd2  32150  lcvexchlem5  32648  pnonsingN  33542  dochnoncon  35003  eldioph2lem2  35647  acsfn1p  36109  nnuzdisj  37615  sumnnodd  37747  sge0less  38271  rhmsscrnghm  40300  rngcresringcat  40304