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

Theorem syl6ss 3515
Description: Subclass transitivity deduction. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
Hypotheses
Ref Expression
syl6ss.1
syl6ss.2
Assertion
Ref Expression
syl6ss

Proof of Theorem syl6ss
StepHypRef Expression
1 syl6ss.1 . 2
2 syl6ss.2 . . 3
32a1i 11 . 2
41, 3sstrd 3513 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  C_wss 3475
This theorem is referenced by:  difss2  3632  rintn0  4421  eqbrrdva  5177  ssxpb  5446  relfld  5538  funssxp  5749  dff2  6043  dff3  6044  fliftf  6213  1stcof  6828  2ndcof  6829  nnunifi  7791  elfiun  7910  marypha1lem  7913  marypha1  7914  ordtypelem7  7970  tcmin  8193  unwf  8249  rankfu  8316  tcrank  8323  aceq3lem  8522  dfac12lem2  8545  ackbij1lem9  8629  ackbij1lem10  8630  ackbij1lem16  8636  fin23lem26  8726  fin23lem27  8729  fin1a2lem6  8806  itunitc  8822  axdc3lem2  8852  ttukeylem5  8914  fpwwe2lem13  9041  canthwelem  9049  pwfseqlem4  9061  wunex2  9137  wunex3  9140  inar1  9174  inatsk  9177  gruina  9217  suprfinzcl  11003  suprzub  11202  uzsupss  11203  uzwo3  11206  rpnnen1lem4  11240  rpnnen1lem5  11241  supxrre  11548  infmxrre  11556  ioodisj  11679  supicclub2  11700  fzossnn0  11856  elfzom1elp1fzo  11883  injresinjlem  11925  uzindi  12091  ssnn0fi  12094  seqcoll  12512  seqcoll2  12513  limsupval2  13303  limsupgre  13304  limsupbnd2  13306  rlimuni  13373  rlimcld2  13401  rlimno1  13476  isercolllem2  13488  isercoll  13490  summolem2a  13537  summolem2  13538  fsumsers  13550  fsumcvg3  13551  prodmolem2a  13741  prodmolem2  13742  zprod  13744  4sqlem11  14473  vdwlem8  14506  vdwlem11  14509  ramub2  14532  0ram  14538  0ram2  14539  0ramcl  14541  ramub1lem2  14545  isohom  15166  funcres2c  15270  resscntz  16369  cntzidss  16375  cntzmhm2  16377  pgpssslw  16634  cntzspan  16850  gsumval3OLD  16908  gsumval3  16911  gsum2d  16999  gsum2dOLD  17000  dprdspan  17074  dprdres  17075  lssintcl  17610  lbsextlem2  17805  lbsextlem3  17806  lbsextlem4  17807  mplbas2  18134  mplbas2OLD  18135  islinds3  18869  fctop  19505  cctop  19507  neitr  19681  ordtbas2  19692  ordtopn1  19695  ordtopn2  19696  lmss  19799  clscon  19931  2ndcdisj  19957  2ndcomap  19959  ptbasfi  20082  txcmplem2  20143  hausdiag  20146  txkgen  20153  basqtop  20212  alexsubb  20546  alexsubALTlem4  20550  tsmsresOLD  20645  tsmsres  20646  tsmsxplem1  20655  tsmsxp  20657  ustrel  20714  utop3cls  20754  prdsmet  20873  metustrelOLD  21058  metustrel  21059  icccmplem2  21328  xrge0tsms  21339  cnmptre  21427  icchmeo  21441  bndth  21458  lebnumlem2  21462  cfilresi  21734  causs  21737  bcthlem5  21767  evthicc  21871  ovolficcss  21881  ovolmge0  21888  ovolgelb  21891  ovollb2lem  21899  ovollb2  21900  ovolunlem1a  21907  ovolunlem1  21908  ovoliunlem1  21913  ovoliunlem2  21914  ovoliun  21916  ovolscalem1  21924  ovolicc1  21927  ovolicc2lem4  21931  ovolicc2  21933  voliunlem2  21961  voliunlem3  21962  ioombl1lem2  21969  ioombl1lem4  21971  uniioovol  21988  uniiccvol  21989  uniioombllem1  21990  uniioombllem2  21992  uniioombllem3  21994  uniioombllem4  21995  uniioombllem6  21997  dyadmbllem  22008  dyadmbl  22009  volcn  22015  vitalilem4  22020  vitalilem5  22021  cnmbf  22066  i1fmul  22103  itg1addlem4  22106  itg2seq  22149  dvbssntr  22304  dvreslem  22313  dvcjbr  22352  dvferm1  22386  dvferm2  22388  cmvth  22392  dvlip  22394  lhop1lem  22414  lhop2  22416  lhop  22417  dvcnvrelem2  22419  dvcnvre  22420  dvfsumle  22422  dvfsumge  22423  dvfsumabs  22424  dvfsumlem2  22428  ftc1a  22438  ftc1lem3  22439  ftc1lem6  22442  itgsubstlem  22449  mdegleb  22464  mdeglt  22465  mdegldg  22466  mdegxrcl  22467  mdegcl  22469  deg1mul3le  22517  ig1pdvds  22577  plyeq0lem  22607  aannenlem2  22725  aalioulem3  22730  taylf  22756  taylthlem2  22769  pserulm  22817  psercn2  22818  psercn  22821  reeff1olem  22841  efcvx  22844  loglesqrt  23132  rlimcnp  23295  xrlimcnp  23298  jensen  23318  wilthlem2  23343  vmadivsumb  23668  pntrsumo1  23750  pntlem3  23794  perpln2  24088  axcontlem10  24276  usgraexmpl  24401  nmoxr  25681  nmooge0  25682  nmoolb  25686  nmoubi  25687  ubthlem1  25786  shmodi  26308  nmopxr  26785  nmfnxr  26798  nmoplb  26826  nmopub  26827  nmfnlb  26843  nmfnleub  26844  nmopun  26933  branmfn  27024  mdslj1i  27238  hatomistici  27281  suppss2f  27477  xppreima2  27488  fpwrelmap  27556  fzssnn  27595  xrge0tsmsd  27775  metideq  27872  metider  27873  pstmfval  27875  sigaclci  28132  insiga  28137  eulerpartlemgs2  28319  ballotlemsima  28454  signsply0  28508  rescon  28691  cvmliftlem8  28737  cvmlift3lem6  28769  mclsssvlem  28922  mclsind  28930  mclsppslem  28943  nofulllem5  29466  heicant  30049  mblfinlem2  30052  mblfinlem3  30053  mblfinlem4  30054  ismblfin  30055  itg2gt0cn  30070  ftc1cnnc  30089  ftc1anclem3  30092  ftc1anclem7  30096  ftc1anclem8  30097  ftc1anc  30098  areacirclem2  30108  areacirclem3  30109  areacirclem4  30110  ivthALT  30153  neibastop1  30177  topjoin  30183  totbndbnd  30285  prdsbnd  30289  heiborlem1  30307  rrnequiv  30331  reheibor  30335  iccbnd  30336  rmxyelqirr  30846  ttac  30978  hbtlem6  31078  hbt  31079  itgpowd  31182  limciccioolb  31627  limcicciooub  31643  limcleqr  31650  cncfiooicclem1  31696  ibliccsinexp  31749  iblioosinexp  31751  itgcoscmulx  31768  itgsincmulx  31773  itgsubsticclem  31774  itgiccshift  31779  itgperiod  31780  itgsbtaddcnst  31781  stoweidlem34  31816  stoweidlem59  31841  dirkeritg  31884  dirkercncflem2  31886  fourierdlem20  31909  fourierdlem31  31920  fourierdlem39  31928  fourierdlem42  31931  fourierdlem46  31935  fourierdlem52  31941  fourierdlem53  31942  fourierdlem60  31949  fourierdlem61  31950  fourierdlem62  31951  fourierdlem68  31957  fourierdlem76  31965  fourierdlem85  31974  fourierdlem88  31977  fourierdlem89  31978  fourierdlem90  31979  fourierdlem91  31980  fourierdlem93  31982  fourierdlem94  31983  fourierdlem103  31992  fourierdlem104  31993  fourierdlem111  32000  fouriersw  32014  etransclem46  32063  etransclem48  32065  bnj1145  34049  bnj1137  34051  bnj1136  34053  pmapssbaN  35484  2polssN  35639  paddunN  35651  poldmj1N  35652  ispsubcl2N  35671  psubclinN  35672  paddatclN  35673  poml4N  35677  diaglbN  36782  diaintclN  36785  dibglbN  36893  dibintclN  36894  dicssdvh  36913  dihvalrel  37006  dochexmidlem4  37190  cnvtrrel  37782  rp-imass  37795
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