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

Theorem sstri 3512
Description: Subclass transitivity inference. (Contributed by NM, 5-May-2000.)
Hypotheses
Ref Expression
sstri.1
sstri.2
Assertion
Ref Expression
sstri

Proof of Theorem sstri
StepHypRef Expression
1 sstri.1 . 2
2 sstri.2 . 2
3 sstr2 3510 . 2
41, 2, 3mp2 9 1
Colors of variables: wff setvar class
Syntax hints:  C_wss 3475
This theorem is referenced by:  snsstp1  4181  snsstp2  4182  uniintsn  4324  ssrnres  5450  cossxp  5535  foimacnv  5838  ssimaex  5938  riotassuniOLD  6294  oprabss  6388  dmexg  6731  rnexg  6732  fabexg  6756  fparlem3  6902  fparlem4  6903  snopsuppss  6933  tposssxp  6978  mapsspw  7474  sbthlem5  7651  sbthlem7  7653  cnvimamptfin  7841  marypha1lem  7913  ordtypelem4  7967  hartogslem1  7988  tc2  8194  tz9.12lem1  8226  rankval4  8306  rankxpl  8314  rankmapu  8317  rankxplim  8318  infxpenlem  8412  ackbij1lem18  8638  cflm  8651  fin23lem29  8742  hsmexlem4  8830  hsmexlem5  8831  brdom3  8927  brdom5  8928  brdom4  8929  smobeth  8982  pwfseqlem3  9059  wundm  9127  wunrn  9128  wunex2  9137  ltsopi  9287  dmaddpi  9289  dmmulpi  9290  nqerf  9329  ltrelxr  9669  nnsscn  10566  nn0sscn  10825  uzwo2  11175  uzinfmi  11190  infmssuzle  11193  infmssuzcl  11194  uzwo3  11206  nn0ssq  11219  nnssq  11220  qsscn  11222  rpnnen1lem3  11239  rpnnen1lem5  11241  dflt2  11383  fzval2  11704  fzof  11826  fzossnn  11870  fzo0ssnn0  11896  injresinj  11926  flval3  11951  uzsup  11990  uzrdgfni  12069  expcl2lem  12178  rpexpcl  12185  expge0  12202  expge1  12203  hashxrcl  12429  seqcoll  12512  wrdexg  12557  sqrlem3  13078  limsupval2  13303  limsupgre  13304  rlimpm  13323  rlimclim  13369  isercolllem1  13487  isercolllem2  13488  isercoll  13490  caurcvg  13499  caucvg  13501  summolem2a  13537  summolem2  13538  zsum  13540  fsumcvg3  13551  fsumrpcl  13559  fsumge0  13609  climfsum  13634  ackbijnn  13640  prodmolem2a  13741  prodmolem2  13742  zprod  13744  fprodrpcl  13763  divalglem8  14058  sadaddlem  14116  isprm3  14226  maxprmfct  14254  pclem  14362  prmreclem1  14434  prmreclem2  14435  prmreclem3  14436  1arith  14445  4sqlem11  14473  ramtlecl  14518  ramcl2lem  14527  ramxrcl  14535  cshwshashlem1  14580  structfn  14645  strlemor1  14724  strleun  14727  srngbase  14753  srngplusg  14754  srngmulr  14755  lmodbase  14762  lmodplusg  14763  lmodsca  14764  ipsbase  14769  ipsaddg  14770  ipsmulr  14771  ipssca  14772  ipsvsca  14773  ipsip  14774  phlbase  14779  phlplusg  14780  phlsca  14781  phlvsca  14782  phlip  14783  odrngbas  14805  odrngplusg  14806  odrngmulr  14807  odrngtset  14808  odrngle  14809  odrngds  14810  prdsval  14852  prdssca  14853  prdsbas  14854  prdsplusg  14855  prdsmulr  14856  prdsvsca  14857  prdsip  14858  prdsle  14859  prdsds  14861  prdstset  14863  prdshom  14864  prdsco  14865  imasbas  14909  imasds  14910  imasplusg  14914  imasmulr  14915  imassca  14916  imasvsca  14917  imasip  14918  imastset  14919  imasle  14920  wunfunc  15268  fullfunc  15275  fthfunc  15276  isfull  15279  isfth  15283  wunnat  15325  dmcoass  15393  catcisolem  15433  catciso  15434  catcoppccl  15435  catcfuccl  15436  catcxpccl  15476  ipobas  15785  ipolerval  15786  ipotset  15787  psdmrn  15837  psss  15844  ledm  15854  lern  15855  dirdm  15864  dirge  15867  mvdco  16470  f1omvdconj  16471  gexex  16859  gsumval3OLD  16908  gsumval3  16911  gsumzaddlemOLD  16936  lssacs  17613  asplss  17978  aspsubrg  17980  psrass1lem  18029  psrbas  18030  psrbasOLD  18031  psrplusg  18034  psrmulr  18037  psrsca  18042  psrvscafval  18043  psrass1  18060  psrass23l  18063  psrcom  18064  psrass23  18065  psropprmul  18279  coe1mul2  18310  cnfldbas  18424  cnfldadd  18425  cnfldmul  18426  cnfldcj  18427  cnfldtset  18428  cnfldle  18429  cnfldds  18430  cnfldunif  18431  rge0srg  18487  zntoslem  18595  ofco2  18953  leordtval2  19713  lmbrf  19761  lmres  19801  fiuncmp  19904  comppfsc  20033  1stckgenlem  20054  kgencn3  20059  ptbasfi  20082  xkoopn  20090  txcnmpt  20125  txkgen  20153  opnfbas  20343  fmfnfmlem4  20458  tsmsxplem1  20655  trust  20732  restutop  20740  nmoffn  21218  nmofval  21221  nmogelb  21223  nmolb  21224  nmof  21226  qtopbas  21266  tgqioo  21305  re2ndc  21306  iitopon  21383  dfii3  21387  iimulcn  21438  cnheiborlem  21454  bndth  21458  lebnumii  21466  reparphti  21497  pcoass  21524  cphsqrtcl  21631  lmmbrf  21701  iscauf  21719  caucfil  21722  lmclimf  21742  rrxmval  21832  rrxmet  21835  ovolfioo  21879  ovolficc  21880  ovolficcss  21881  ovolfsf  21883  ovollb  21890  ovolicc2lem3  21930  ovolicc2lem4  21931  ovolicc2  21933  volf  21940  volsup  21966  ovolfs2  21980  uniiccdif  21987  uniioovol  21988  uniiccvol  21989  uniioombllem2  21992  uniioombllem3a  21993  uniioombllem3  21994  uniioombllem4  21995  uniioombllem5  21996  uniioombl  21998  dyadmbllem  22008  dyadmbl  22009  opnmbllem  22010  opnmblALT  22012  volsup2  22014  vitalilem4  22020  vitalilem5  22021  vitali  22022  mbfimaopnlem  22062  mbflimsup  22073  i1f0  22094  i1f1  22097  itg11  22098  itg2mulc  22154  itg2gt0  22167  ellimc2  22281  limcresi  22289  dvreslem  22313  dvres2lem  22314  dvaddbr  22341  dvmulbr  22342  dvlipcn  22395  c1liplem1  22397  lhop1lem  22414  lhop1  22415  lhop2  22416  lhop  22417  dvfsumrlim  22432  ftc1cn  22444  itgsubstlem  22449  itgsubst  22450  mdegleb  22464  mdeglt  22465  mdegldg  22466  mdegxrcl  22467  mdegcl  22469  mdegaddle  22474  mdegmullem  22478  deg1mul3le  22517  ig1peu  22572  ig1pdvds  22577  aacjcl  22723  aannenlem2  22725  aannenlem3  22726  aalioulem2  22729  taylfval  22754  radcnvcl  22812  radcnvlt1  22813  radcnvle  22815  abelth  22836  abelth2  22837  pilem2  22847  pilem3  22848  pige3  22910  recosf1o  22922  resinf1o  22923  tanord1  22924  logcn  23028  dvlog  23032  dvlog2lem  23033  efopn  23039  logtayl  23041  cxpcn3  23122  loglesqrt  23132  ssscongptld  23156  leibpi  23273  efrlim  23299  jensenlem1  23316  jensenlem2  23317  jensen  23318  amgm  23320  ftalem5  23350  efnnfsumcl  23376  efchtdvds  23433  dvdsmulf1o  23470  fsumdvdsmul  23471  lgsfcl2  23577  2sqlem6  23644  2sqlem8  23647  2sqlem9  23648  rpvmasumlem  23672  rpvmasum2  23697  dchrisum0re  23698  dchrisum0lem3  23704  dchrisum0  23705  rplogsum  23712  dirith2  23713  axtgcgrrflx  23859  axtgcgrid  23860  axtgsegcon  23861  axtg5seg  23862  axtgbtwnid  23863  axtgpasch  23864  axtgcont1  23865  motcgrg  23931  tglng  23933  umgrass  24319  constr3pthlem1  24655  disjxwwlkn  24745  nmlno0lem  25708  hlimcaui  26154  chsspwh  26165  shsss  26231  chintcli  26249  shsleji  26288  shub1i  26292  shsval2i  26305  lejdii  26456  spanuni  26462  sshhococi  26464  spansnpji  26496  osumcori  26561  5oai  26579  3oalem6  26585  3oai  26586  pjssmii  26599  mayete3i  26646  mayete3iOLD  26647  mayetes3i  26648  nmlnop0iALT  26914  imaelshi  26977  pjnmopi  27067  pjclem1  27114  pjci  27119  mdslmd1lem1  27244  shatomistici  27280  hatomistici  27281  chpssati  27282  xppreima  27487  iundisjfi  27601  iundisj2fi  27602  xrsmulgzz  27666  fsumrp0cl  27685  gsummpt2co  27771  xrge0slmod  27834  unitsscn  27878  ordtconlem1  27906  xrge0iifhom  27919  lmlimxrge0  27930  lmxrge0  27934  esumcst  28071  esumpfinvallem  28080  esumpfinval  28081  esumpfinvalf  28082  esumcvg  28092  imambfm  28233  elmbfmvol2  28238  sxbrsigalem3  28243  sxbrsigalem2  28257  sxbrsigalem4  28258  sitgclg  28284  eulerpartlem1  28306  eulerpartlemgvv  28315  eulerpartlemgh  28317  eulerpartlemgf  28318  ballotlemfc0  28431  ballotlemfcc  28432  ballotlemiex  28440  ballotlemsup  28443  ballotlemsdom  28450  ballotlemsima  28454  ballotlemrv2  28460  ballotth  28476  signsplypnf  28507  signsply0  28508  lgamgulmlem2  28572  subfacp1lem2a  28624  erdszelem4  28638  erdszelem5  28639  erdszelem7  28641  erdszelem8  28642  kur14lem7  28656  kur14lem9  28658  cvxpcon  28687  cvxscon  28688  rescon  28691  iccllyscon  28695  rprisefaccl  29145  txpss3v  29528  txprel  29529  limitssson  29561  onint1  29914  opnmbllem0  30050  mblfinlem1  30051  mblfinlem2  30052  mblfinlem3  30053  mblfinlem4  30054  ismblfin  30055  mbfposadd  30062  cnambfre  30063  itg2addnc  30069  ftc1cnnclem  30088  ftc1cnnc  30089  ftc1anclem3  30092  ftc1anclem7  30096  ftc1anc  30098  ftc2nc  30099  dvreasin  30105  dvreacos  30106  areacirclem1  30107  areacirclem2  30108  areacirc  30112  finminlem  30136  tailf  30193  filnetlem3  30198  caures  30253  reheibor  30335  diophin  30706  4rexfrabdioph  30731  6rexfrabdioph  30732  irrapxlem1  30758  irrapx1  30764  monotuz  30877  jm2.27dlem5  30955  hbtlem2  31073  algbase  31127  algaddg  31128  algmulr  31129  algsca  31130  algvsca  31131  itgpowd  31182  arearect  31183  areaquad  31184  lhe4.4ex1a  31234  uzmptshftfval  31251  binomcxplemdvbinom  31258  binomcxplemcvg  31259  binomcxplemnotnn0  31261  fzisoeu  31500  fzsscn  31514  fzssre  31518  ioosscn  31527  fprodge0  31597  fprodge1  31598  limcresiooub  31648  limcresioolb  31649  limcleqr  31650  limclner  31657  limclr  31661  icccncfext  31690  cncficcgt0  31691  ioodvbdlimc1lem2  31729  ioodvbdlimc2lem  31731  dvnprodlem1  31743  dvnprodlem2  31744  itgsin0pilem1  31748  itgsinexplem1  31752  itgsinexp  31753  dirkercncflem2  31886  fourierdlem16  31905  fourierdlem18  31907  fourierdlem20  31909  fourierdlem21  31910  fourierdlem22  31911  fourierdlem25  31914  fourierdlem37  31926  fourierdlem42  31931  fourierdlem50  31939  fourierdlem52  31941  fourierdlem62  31951  fourierdlem64  31953  fourierdlem66  31955  fourierdlem68  31957  fourierdlem74  31963  fourierdlem75  31964  fourierdlem76  31965  fourierdlem79  31968  fourierdlem83  31972  fourierdlem95  31984  fourierdlem101  31990  fourierdlem102  31991  fourierdlem103  31992  fourierdlem104  31993  fourierdlem112  32001  fourierdlem114  32003  sqwvfoura  32011  sqwvfourb  32012  fouriersw  32014  etransclem24  32041  etransclem48  32065  oddibas  32501  2zrngbas  32742  2zrng0  32744  aacllem  33216  relopabVD  33701  bnj1145  34049  bnj1286  34075  bj-unrab  34494  bj-2upln1upl  34582  bj-rrvecsscmn  34668  atlatmstc  35044  atlatle  35045  pmaple  35485  sspadd1  35539  sspadd2  35540  taupilem2  37697  taupi  37698  xptrrel  37775  trclubg  37785  idhe  37810
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-in 3482  df-ss 3489
  Copyright terms: Public domain W3C validator