Theorem ssrin 3572

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 3347	. . . 4 |- ( A C_ B -> ( x e. A -> x e. B ) )
2	1	anim1d 561	. . 3 |- ( A C_ B -> ( ( x e. A /\ x e. C ) -> ( x e. B /\ x e. C ) ) )
3		elin 3536	. . 3 |- ( x e. ( A i^i C ) <-> ( x e. A /\ x e. C ) )
4		elin 3536	. . 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 3359	1 |- ( A C_ B -> ( A i^i C ) C_ ( B i^i C ) )

Syntax hints:   -> wi 4   /\ wa 369   e. wcel 1761   i^i cin 3324   C_ wss 3325

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1713  ax-7 1733  ax-10 1780  ax-11 1785  ax-12 1797  ax-13 1948  ax-ext 2422

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1367  df-ex 1592  df-nf 1595  df-sb 1706  df-clab 2428  df-cleq 2434  df-clel 2437  df-nfc 2566  df-v 2972  df-in 3332  df-ss 3339

This theorem is referenced by:  sslin  3573  ss2in  3574  ssdisj  3725  ssdifin0  3757  ssres  5133  sbthlem7  7423  onsdominel  7456  phplem2  7487  infdifsn  7858  fictb  8410  fin23lem23  8491  ttukeylem2  8675  limsupgord  12946  xpsc1  14495  isacs1i  14591  rescabs  14742  lsmdisj  16171  dmdprdsplit2lem  16534  pjfval  18090  pjpm  18092  obselocv  18112  tgss  18532  neindisj2  18686  restbas  18721  neitr  18743  restcls  18744  restntr  18745  nrmsep  18920  1stcrest  19016  cldllycmp  19058  kgencn3  19090  trfbas2  19375  fclsneii  19549  fclsrest  19556  fcfnei  19567  cnextcn  19598  tsmsresOLD  19676  tsmsres  19677  trust  19763  restutopopn  19772  trcfilu  19828  metrest  20058  reperflem  20354  metdseq0  20389  iundisj2  20989  uniioombllem3  21024  ellimc3  21313  limcflf  21315  lhop1lem  21444  ppisval  22400  ppisval2  22401  ppinprm  22449  chtnprm  22451  chtwordi  22453  ppiwordi  22459  chpub  22518  chebbnd1lem1  22677  chtppilimlem1  22681  orthin  24784  3oalem6  25005  mdbr2  25635  mdslle1i  25656  mdslle2i  25657  mdslj1i  25658  mdslj2i  25659  mdsl2i  25661  mdslmd1lem1  25664  mdslmd1lem2  25665  mdslmd3i  25671  mdexchi  25674  sumdmdlem  25757  iundisj2f  25867  iundisj2fi  26014  eulerpartlemn  26694  predpredss  27560  ismblfin  28357  sstotbnd2  28598  eldioph2lem2  29024  acsfn1p  29481  bnj1177  31831  lcvexchlem5  32405  pnonsingN  33299  dochnoncon  34758