Theorem ssrin 3578

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 3353	. . . 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 3542	. . 3 |- ( x e. ( A i^i C ) <-> ( x e. A /\ x e. C ) )
4		elin 3542	. . 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 3365	1 |- ( A C_ B -> ( A i^i C ) C_ ( B i^i C ) )

Syntax hints:   -> wi 4   /\ wa 369   e. wcel 1756   i^i cin 3330   C_ wss 3331

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2571  df-v 2977  df-in 3338  df-ss 3345

This theorem is referenced by:  sslin  3579  ss2in  3580  ssdisj  3731  ssdifin0  3763  ssres  5139  sbthlem7  7430  onsdominel  7463  phplem2  7494  infdifsn  7865  fictb  8417  fin23lem23  8498  ttukeylem2  8682  limsupgord  12953  xpsc1  14502  isacs1i  14598  rescabs  14749  lsmdisj  16181  dmdprdsplit2lem  16547  pjfval  18134  pjpm  18136  obselocv  18156  tgss  18576  neindisj2  18730  restbas  18765  neitr  18787  restcls  18788  restntr  18789  nrmsep  18964  1stcrest  19060  cldllycmp  19102  kgencn3  19134  trfbas2  19419  fclsneii  19593  fclsrest  19600  fcfnei  19611  cnextcn  19642  tsmsresOLD  19720  tsmsres  19721  trust  19807  restutopopn  19816  trcfilu  19872  metrest  20102  reperflem  20398  metdseq0  20433  iundisj2  21033  uniioombllem3  21068  ellimc3  21357  limcflf  21359  lhop1lem  21488  ppisval  22444  ppisval2  22445  ppinprm  22493  chtnprm  22495  chtwordi  22497  ppiwordi  22503  chpub  22562  chebbnd1lem1  22721  chtppilimlem1  22725  orthin  24852  3oalem6  25073  mdbr2  25703  mdslle1i  25724  mdslle2i  25725  mdslj1i  25726  mdslj2i  25727  mdsl2i  25729  mdslmd1lem1  25732  mdslmd1lem2  25733  mdslmd3i  25739  mdexchi  25742  sumdmdlem  25825  iundisj2f  25935  iundisj2fi  26084  eulerpartlemn  26767  predpredss  27634  ismblfin  28435  sstotbnd2  28676  eldioph2lem2  29102  acsfn1p  29559  bnj1177  32000  lcvexchlem5  32686  pnonsingN  33580  dochnoncon  35039