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

Theorem ssrin 3428
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 3208 . . . 4  |-  ( A 
C_  B  ->  (
x  e.  A  ->  x  e.  B )
)
21anim1d 547 . . 3  |-  ( A 
C_  B  ->  (
( x  e.  A  /\  x  e.  C
)  ->  ( x  e.  B  /\  x  e.  C ) ) )
3 elin 3392 . . 3  |-  ( x  e.  ( A  i^i  C )  <->  ( x  e.  A  /\  x  e.  C ) )
4 elin 3392 . . 3  |-  ( x  e.  ( B  i^i  C )  <->  ( x  e.  B  /\  x  e.  C ) )
52, 3, 43imtr4g 261 . 2  |-  ( A 
C_  B  ->  (
x  e.  ( A  i^i  C )  ->  x  e.  ( B  i^i  C ) ) )
65ssrdv 3219 1  |-  ( A 
C_  B  ->  ( A  i^i  C )  C_  ( B  i^i  C ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    e. wcel 1701    i^i cin 3185    C_ wss 3186
This theorem is referenced by:  sslin  3429  ss2in  3430  ssdisj  3538  ssdifin0  3569  ssres  5018  sbthlem7  7020  onsdominel  7053  phplem2  7084  infdifsn  7402  fictb  7916  fin23lem23  7997  ttukeylem2  8182  limsupgord  11993  xpsc1  13512  isacs1i  13608  rescabs  13759  lsmdisj  15039  dmdprdsplit2lem  15329  pjfval  16662  pjpm  16664  obselocv  16684  tgss  16762  neindisj2  16916  restbas  16945  restcls  16967  restntr  16968  nrmsep  17141  1stcrest  17235  cldllycmp  17277  kgencn3  17309  trfbas2  17590  fclsneii  17764  fclsrest  17771  fcfnei  17782  tsmsres  17878  metrest  18122  reperflem  18375  metdseq0  18410  iundisj2  18959  uniioombllem3  18993  ellimc3  19282  limcflf  19284  lhop1lem  19413  ppisval  20394  ppisval2  20395  ppinprm  20443  chtnprm  20445  chtwordi  20447  ppiwordi  20453  chpub  20512  chebbnd1lem1  20671  chtppilimlem1  20675  orthin  22080  3oalem6  22301  mdbr2  22931  mdslle1i  22952  mdslle2i  22953  mdslj1i  22954  mdslj2i  22955  mdsl2i  22957  mdslmd1lem1  22960  mdslmd1lem2  22961  mdslmd3i  22967  mdexchi  22970  sumdmdlem  23053  iundisj2f  23172  iundisj2fi  23302  trust  23441  restutopopn  23449  predpredss  24557  sstotbnd2  25646  eldioph2lem2  25988  acsfn1p  26655  bnj1177  28547  lcvexchlem5  29046  pnonsingN  29940  dochnoncon  31399
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1537  ax-5 1548  ax-17 1607  ax-9 1645  ax-8 1666  ax-6 1720  ax-7 1725  ax-11 1732  ax-12 1897  ax-ext 2297
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1533  df-nf 1536  df-sb 1640  df-clab 2303  df-cleq 2309  df-clel 2312  df-nfc 2441  df-v 2824  df-in 3193  df-ss 3200
  Copyright terms: Public domain W3C validator