Theorem ssrin 3709

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 562	. . 3 |- ( A C_ B -> ( ( x e. A /\ x e. C ) -> ( x e. B /\ x e. C ) ) )
3		elin 3673	. . 3 |- ( x e. ( A i^i C ) <-> ( x e. A /\ x e. C ) )
4		elin 3673	. . 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 367   e. wcel 1823   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 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432

This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-v 3108  df-in 3468  df-ss 3475

This theorem is referenced by:  sslin  3710  ss2in  3711  ssdisj  3864  ssdifin0  3897  ssres  5287  sbthlem7  7626  onsdominel  7659  phplem2  7690  infdifsn  8064  fictb  8616  fin23lem23  8697  ttukeylem2  8881  limsupgord  13377  xpsc1  15050  isacs1i  15146  rescabs  15321  lsmdisj  16898  dmdprdsplit2lem  17289  pjfval  18910  pjpm  18912  obselocv  18932  tgss  19637  neindisj2  19791  restbas  19826  neitr  19848  restcls  19849  restntr  19850  nrmsep  20025  1stcrest  20120  cldllycmp  20162  kgencn3  20225  trfbas2  20510  fclsneii  20684  fclsrest  20691  fcfnei  20702  cnextcn  20733  tsmsresOLD  20811  tsmsres  20812  trust  20898  restutopopn  20907  trcfilu  20963  metrest  21193  reperflem  21489  metdseq0  21524  iundisj2  22125  uniioombllem3  22160  ellimc3  22449  limcflf  22451  lhop1lem  22580  ppisval  23575  ppisval2  23576  ppinprm  23624  chtnprm  23626  chtwordi  23628  ppiwordi  23634  chpub  23693  chebbnd1lem1  23852  chtppilimlem1  23856  orthin  26562  3oalem6  26783  mdbr2  27413  mdslle1i  27434  mdslle2i  27435  mdslj1i  27436  mdslj2i  27437  mdsl2i  27439  mdslmd1lem1  27442  mdslmd1lem2  27443  mdslmd3i  27449  mdexchi  27452  sumdmdlem  27535  iundisj2f  27660  iundisj2fi  27836  esumrnmpt2  28297  eulerpartlemn  28584  predpredss  29490  ismblfin  30295  sstotbnd2  30510  eldioph2lem2  30933  acsfn1p  31389  sumnnodd  31875  rhmsscrnghm  33088  rngcresringcat  33092  bnj1177  34463  lcvexchlem5  35160  pnonsingN  36054  dochnoncon  37515