Theorem ssrin 3625

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 3396	. . . 4 |- ( A C_ B -> ( x e. A -> x e. B ) )
2	1	anim1d 566	. . 3 |- ( A C_ B -> ( ( x e. A /\ x e. C ) -> ( x e. B /\ x e. C ) ) )
3		elin 3587	. . 3 |- ( x e. ( A i^i C ) <-> ( x e. A /\ x e. C ) )
4		elin 3587	. . 3 |- ( x e. ( B i^i C ) <-> ( x e. B /\ x e. C ) )
5	2, 3, 4	3imtr4g 273	. 2 |- ( A C_ B -> ( x e. ( A i^i C ) -> x e. ( B i^i C ) ) )
6	5	ssrdv 3408	1 |- ( A C_ B -> ( A i^i C ) C_ ( B i^i C ) )

Syntax hints:   -> wi 4   /\ wa 370   e. wcel 1872   i^i cin 3373   C_ wss 3374

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2058  ax-ext 2403

This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-clab 2410  df-cleq 2416  df-clel 2419  df-nfc 2553  df-v 3019  df-in 3381  df-ss 3388

This theorem is referenced by:  sslin  3626  ss2in  3627  ssdisj  3782  ssdifin0  3817  ssres  5087  predpredss  5343  sbthlem7  7636  onsdominel  7669  phplem2  7700  infdifsn  8109  fictb  8621  fin23lem23  8702  ttukeylem2  8886  limsupgord  13466  xpsc1  15405  isacs1i  15501  rescabs  15676  lsmdisj  17269  dmdprdsplit2lem  17616  pjfval  19206  pjpm  19208  obselocv  19228  tgss  19921  neindisj2  20076  restbas  20111  neitr  20133  restcls  20134  restntr  20135  nrmsep  20310  1stcrest  20405  cldllycmp  20447  kgencn3  20510  trfbas2  20795  fclsneii  20969  fclsrest  20976  fcfnei  20987  cnextcn  21019  tsmsres  21095  trust  21181  restutopopn  21190  trcfilu  21246  metrest  21476  reperflem  21773  metdseq0  21808  metdseq0OLD  21823  iundisj2  22439  uniioombllem3  22480  ellimc3  22771  limcflf  22773  lhop1lem  22902  ppisval  23967  ppisval2  23968  ppinprm  24016  chtnprm  24018  chtwordi  24020  ppiwordi  24026  chpub  24085  chebbnd1lem1  24244  chtppilimlem1  24248  orthin  27036  3oalem6  27257  mdbr2  27886  mdslle1i  27907  mdslle2i  27908  mdslj1i  27909  mdslj2i  27910  mdsl2i  27912  mdslmd1lem1  27915  mdslmd1lem2  27916  mdslmd3i  27922  mdexchi  27925  sumdmdlem  28008  iundisj2f  28141  iundisj2fi  28318  esumrnmpt2  28836  eulerpartlemn  29161  bnj1177  29762  poimirlem3  31850  poimirlem29  31876  ismblfin  31888  sstotbnd2  32013  lcvexchlem5  32516  pnonsingN  33410  dochnoncon  34871  eldioph2lem2  35515  acsfn1p  35978  nnuzdisj  37475  sumnnodd  37593  sge0less  38085  rhmsscrnghm  39619  rngcresringcat  39623