MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ssrin Structured version   Unicode version

Theorem ssrin 3566
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.
StepHypRef Expression
1 ssel 3342 . . . 4  |-  ( A 
C_  B  ->  (
x  e.  A  ->  x  e.  B )
)
21anim1d 548 . . 3  |-  ( A 
C_  B  ->  (
( x  e.  A  /\  x  e.  C
)  ->  ( x  e.  B  /\  x  e.  C ) ) )
3 elin 3530 . . 3  |-  ( x  e.  ( A  i^i  C )  <->  ( x  e.  A  /\  x  e.  C ) )
4 elin 3530 . . 3  |-  ( x  e.  ( B  i^i  C )  <->  ( x  e.  B  /\  x  e.  C ) )
52, 3, 43imtr4g 262 . 2  |-  ( A 
C_  B  ->  (
x  e.  ( A  i^i  C )  ->  x  e.  ( B  i^i  C ) ) )
65ssrdv 3354 1  |-  ( A 
C_  B  ->  ( A  i^i  C )  C_  ( B  i^i  C ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 359    e. wcel 1725    i^i cin 3319    C_ wss 3320
This theorem is referenced by:  sslin  3567  ss2in  3568  ssdisj  3677  ssdifin0  3709  ssres  5172  sbthlem7  7223  onsdominel  7256  phplem2  7287  infdifsn  7611  fictb  8125  fin23lem23  8206  ttukeylem2  8390  limsupgord  12266  xpsc1  13786  isacs1i  13882  rescabs  14033  lsmdisj  15313  dmdprdsplit2lem  15603  pjfval  16933  pjpm  16935  obselocv  16955  tgss  17033  neindisj2  17187  restbas  17222  neitr  17244  restcls  17245  restntr  17246  nrmsep  17421  1stcrest  17516  cldllycmp  17558  kgencn3  17590  trfbas2  17875  fclsneii  18049  fclsrest  18056  fcfnei  18067  cnextcn  18098  tsmsres  18173  trust  18259  restutopopn  18268  trcfilu  18324  metrest  18554  reperflem  18849  metdseq0  18884  iundisj2  19443  uniioombllem3  19477  ellimc3  19766  limcflf  19768  lhop1lem  19897  ppisval  20886  ppisval2  20887  ppinprm  20935  chtnprm  20937  chtwordi  20939  ppiwordi  20945  chpub  21004  chebbnd1lem1  21163  chtppilimlem1  21167  orthin  22948  3oalem6  23169  mdbr2  23799  mdslle1i  23820  mdslle2i  23821  mdslj1i  23822  mdslj2i  23823  mdsl2i  23825  mdslmd1lem1  23828  mdslmd1lem2  23829  mdslmd3i  23835  mdexchi  23838  sumdmdlem  23921  iundisj2f  24030  iundisj2fi  24153  predpredss  25445  ismblfin  26247  sstotbnd2  26483  eldioph2lem2  26819  acsfn1p  27484  bnj1177  29375  lcvexchlem5  29836  pnonsingN  30730  dochnoncon  32189
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2417
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2423  df-cleq 2429  df-clel 2432  df-nfc 2561  df-v 2958  df-in 3327  df-ss 3334
  Copyright terms: Public domain W3C validator