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

Theorem ssrin 3394
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 3174 . . . 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 3358 . . 3  |-  ( x  e.  ( A  i^i  C )  <->  ( x  e.  A  /\  x  e.  C ) )
4 elin 3358 . . 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 3185 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 1684    i^i cin 3151    C_ wss 3152
This theorem is referenced by:  sslin  3395  ss2in  3396  ssdisj  3504  ssdifin0  3535  ssres  4981  sbthlem7  6977  onsdominel  7010  phplem2  7041  infdifsn  7357  fictb  7871  fin23lem23  7952  ttukeylem2  8137  limsupgord  11946  xpsc1  13463  isacs1i  13559  rescabs  13710  lsmdisj  14990  dmdprdsplit2lem  15280  pjfval  16606  pjpm  16608  obselocv  16628  tgss  16706  neindisj2  16860  restbas  16889  restcls  16911  restntr  16912  nrmsep  17085  1stcrest  17179  cldllycmp  17221  kgencn3  17253  trfbas2  17538  fclsneii  17712  fclsrest  17719  fcfnei  17730  tsmsres  17826  metrest  18070  reperflem  18323  metdseq0  18358  iundisj2  18906  uniioombllem3  18940  ellimc3  19229  limcflf  19231  lhop1lem  19360  ppisval  20341  ppisval2  20342  ppinprm  20390  chtnprm  20392  chtwordi  20394  ppiwordi  20400  chpub  20459  chebbnd1lem1  20618  chtppilimlem1  20622  orthin  22025  3oalem6  22246  mdbr2  22876  mdslle1i  22897  mdslle2i  22898  mdslj1i  22899  mdslj2i  22900  mdsl2i  22902  mdslmd1lem1  22905  mdslmd1lem2  22906  mdslmd3i  22912  mdexchi  22915  sumdmdlem  22998  iundisj2fi  23364  iundisj2f  23366  predpredss  24172  hdrmp  25706  sstotbnd2  26498  eldioph2lem2  26840  acsfn1p  27507  bnj1177  29036  lcvexchlem5  29228  pnonsingN  30122  dochnoncon  31581
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-v 2790  df-in 3159  df-ss 3166
  Copyright terms: Public domain W3C validator