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

Theorem ssrin 3722
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

Proof of Theorem ssrin
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 ssel 3497 . . . 4
21anim1d 564 . . 3
3 elin 3686 . . 3
4 elin 3686 . . 3
52, 3, 43imtr4g 270 . 2
65ssrdv 3509 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\wa 369  e.wcel 1818  i^icin 3474  C_wss 3475
This theorem is referenced by:  sslin  3723  ss2in  3724  ssdisj  3876  ssdifin0  3909  ssres  5304  sbthlem7  7653  onsdominel  7686  phplem2  7717  infdifsn  8094  fictb  8646  fin23lem23  8727  ttukeylem2  8911  limsupgord  13295  xpsc1  14958  isacs1i  15054  rescabs  15202  lsmdisj  16699  dmdprdsplit2lem  17094  pjfval  18737  pjpm  18739  obselocv  18759  tgss  19470  neindisj2  19624  restbas  19659  neitr  19681  restcls  19682  restntr  19683  nrmsep  19858  1stcrest  19954  cldllycmp  19996  kgencn3  20059  trfbas2  20344  fclsneii  20518  fclsrest  20525  fcfnei  20536  cnextcn  20567  tsmsresOLD  20645  tsmsres  20646  trust  20732  restutopopn  20741  trcfilu  20797  metrest  21027  reperflem  21323  metdseq0  21358  iundisj2  21959  uniioombllem3  21994  ellimc3  22283  limcflf  22285  lhop1lem  22414  ppisval  23377  ppisval2  23378  ppinprm  23426  chtnprm  23428  chtwordi  23430  ppiwordi  23436  chpub  23495  chebbnd1lem1  23654  chtppilimlem1  23658  orthin  26364  3oalem6  26585  mdbr2  27215  mdslle1i  27236  mdslle2i  27237  mdslj1i  27238  mdslj2i  27239  mdsl2i  27241  mdslmd1lem1  27244  mdslmd1lem2  27245  mdslmd3i  27251  mdexchi  27254  sumdmdlem  27337  iundisj2f  27449  iundisj2fi  27602  eulerpartlemn  28320  predpredss  29250  ismblfin  30055  sstotbnd2  30270  eldioph2lem2  30694  acsfn1p  31148  sumnnodd  31636  rhmsscrnghm  32834  rngcresringcat  32838  bnj1177  34062  lcvexchlem5  34763  pnonsingN  35657  dochnoncon  37118
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-v 3111  df-in 3482  df-ss 3489
  Copyright terms: Public domain W3C validator