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

Theorem sstrd 3513
Description: Subclass transitivity deduction. (Contributed by NM, 2-Jun-2004.)
Hypotheses
Ref Expression
sstrd.1
sstrd.2
Assertion
Ref Expression
sstrd

Proof of Theorem sstrd
StepHypRef Expression
1 sstrd.1 . 2
2 sstrd.2 . 2
3 sstr 3511 . 2
41, 2, 3syl2anc 661 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  C_wss 3475
This theorem is referenced by:  syl5ss  3514  syl6ss  3515  ssdif2d  3642  uniintsn  4324  funss  5611  fssxp  5748  knatar  6253  suppssfvOLD  6531  suppssov1OLD  6532  tfisi  6693  suppfnss  6944  suppssov1  6951  suppssfv  6955  tposss  6975  tfrlem1  7064  omwordri  7240  oewordri  7260  oeeui  7270  oaabs2  7313  omopthlem1  7323  ecinxp  7405  sbthlem1  7647  dffi2  7903  hartogslem1  7988  cantnfcl  8107  cantnflt  8112  cantnfp1lem3  8120  cantnflem3  8131  cantnfclOLD  8137  cantnfltOLD  8142  cantnfp1lem3OLD  8146  cantnflem3OLD  8153  cnfcom  8165  cnfcom3lem  8168  cnfcomOLD  8173  cnfcom3lemOLD  8176  rankssb  8287  tskwe  8352  dfac12lem2  8545  dfac12lem3  8546  cfflb  8660  cfcof  8675  ssfin2  8721  hsmexlem4  8830  ttukeylem6  8915  ttukeylem7  8916  fpwwe2lem1  9030  fpwwe2lem8  9036  fpwwe2lem11  9039  fpwwe2lem12  9040  canthnumlem  9047  canthwelem  9049  canthwe  9050  canthp1lem2  9052  pwfseqlem5  9062  wunex2  9137  tsktrss  9160  inttsk  9173  uzwo3  11206  supicc  11697  supiccub  11698  supicclub  11699  seqsplit  12140  seqf1olem2a  12145  seqz  12155  swrdval2  12647  sumss  13546  qshash  13639  incexc  13649  incexc2  13650  prodss  13754  rpnnen2lem11  13958  vdwlem1  14499  ramub1lem1  14544  imasaddvallem  14926  imasvscaf  14936  mrerintcl  14994  ismred2  15000  mremre  15001  mrcuni  15018  mressmrcd  15024  submrc  15025  mrissmrid  15038  mreexexlem2d  15042  isacs2  15050  isacs1i  15054  invss  15155  ssctr  15194  funcres2b  15266  isacs3lem  15796  acsfiindd  15807  acsmapd  15808  acsmap2d  15809  tsrdir  15868  subsubm  15988  gsumwspan  16014  subsubg  16224  subgint  16225  cntzidss  16375  symggen  16495  pmtrdifellem1  16501  pmtrdifellem2  16502  pgpssslw  16634  lsmless1x  16664  lsmless2x  16665  lsmless12  16681  subglsm  16691  gsumval3OLD  16908  gsumval3lem2  16910  gsumzaddlem  16934  gsumzadd  16935  gsumzaddOLD  16937  gsum2d  16999  gsum2dOLD  17000  dmdprdd  17030  dprdfeq0  17062  dprdfeq0OLD  17069  dprdspan  17074  dprdres  17075  dprdss  17076  dprdz  17077  subgdmdprd  17081  subgdprd  17082  dprdsn  17083  dprd2dlem1  17090  dprd2da  17091  dmdprdsplit2lem  17094  dprdsplit  17097  pgpfac1lem2  17126  pgpfac1lem3  17128  pgpfac1lem5  17130  subsubrg  17455  lspss  17630  lspun  17633  lsslsp  17661  lmhmlsp  17695  lsmelval2  17731  lsmssspx  17734  lsppratlem2  17794  lsppratlem3  17795  lsppratlem4  17796  lbsextlem2  17805  lbsextlem3  17806  aspss  17981  ocvlsp  18707  cssmre  18724  obselocv  18759  obslbs  18761  toponmre  19594  neiint  19605  neiss  19610  lpss  19643  lpss3  19645  restopnb  19676  restfpw  19680  neitr  19681  restcls  19682  restntr  19683  restlp  19684  ordtbas  19693  pnfnei  19721  mnfnei  19722  iscnp4  19764  cnclsi  19773  isreg2  19878  discmp  19898  cmpcld  19902  uncmp  19903  sscmp  19905  hauscmplem  19906  cmpfi  19908  iunconlem  19928  clscon  19931  2ndcctbss  19956  restnlly  19983  llyrest  19986  nllyrest  19987  llyidm  19989  nllyidm  19990  cldllycmp  19996  dislly  19998  comppfsc  20033  llycmpkgen2  20051  ptbasfi  20082  txnlly  20138  txcmplem1  20142  tx1stc  20151  xkococnlem  20160  qtopval2  20197  basqtop  20212  tgqtop  20213  qtoprest  20218  kqreglem1  20242  kqreglem2  20243  kqnrmlem1  20244  kqnrmlem2  20245  fsubbas  20368  fgabs  20380  fbasrn  20385  trfil2  20388  trfg  20392  isufil2  20409  trufil  20411  ssufl  20419  ufileu  20420  filufint  20421  fmfnfmlem4  20458  fmfnfm  20459  flimss2  20473  flimss1  20474  fclsfnflim  20528  flimfnfcls  20529  fclscmp  20531  cnpfcfi  20541  alexsubALT  20551  clssubg  20607  clsnsg  20608  tsmsres  20646  ustexsym  20718  ustex2sym  20719  ustex3sym  20720  ustund  20724  ustneism  20726  trust  20732  utoptop  20737  restutopopn  20741  utop2nei  20753  utopreg  20755  cfiluweak  20798  neipcfilu  20799  blssps  20927  blss  20928  blcld  21008  blsscls  21010  met1stc  21024  met2ndci  21025  metustOLD  21070  metust  21071  cfilucfilOLD  21072  cfilucfil  21073  restmetu  21090  tgqioo  21305  xrsblre  21316  reconnlem2  21332  xrge0gsumle  21338  xrge0tsms  21339  rescncf  21401  cnmpt2pc  21428  cnheibor  21455  cnllycmp  21456  lebnum  21464  phtpycn  21483  cfilfcls  21713  iscmet3lem2  21731  cmetss  21753  cncmet  21761  bcthlem4  21766  bcth3  21770  rrxcph  21824  rrxmetlem  21834  minveclem4a  21845  minveclem4  21847  ivthicc  21870  ovollb  21890  ovollb2lem  21899  ovollb2  21900  nulmbl2  21947  ioorcl2  21981  uniioombllem3  21994  uniioombllem4  21995  uniioombllem5  21996  opnmbllem  22010  volcn  22015  volivth  22016  mbfeqalem  22049  itg10a  22117  mbfi1fseqlem4  22125  ditgcl  22262  ditgswap  22263  ditgsplitlem  22264  limcflf  22285  limcres  22290  dvbss  22305  dvbsss  22306  perfdvf  22307  dvreslem  22313  dvres2lem  22314  dvres3  22317  dvcnp  22322  dvcnp2  22323  dvcn  22324  dvnff  22326  dvn2bss  22333  dvnres  22334  cpnord  22338  dvaddbr  22341  dvmulbr  22342  dvcobr  22349  dvnfre  22355  dvmptres2  22365  dvmptntr  22374  dvcnvlem  22377  dvcnv  22378  dvferm1lem  22385  dvferm2lem  22387  dvlip  22394  dvlipcn  22395  dvlip2  22396  c1liplem1  22397  dvgt0lem1  22403  lhop1lem  22414  lhop  22417  dvcnvrelem1  22418  dvcnvrelem2  22419  dvcnvre  22420  dvfsumle  22422  dvfsumge  22423  dvfsumabs  22424  ftc1lem1  22436  ftc1lem2  22437  ftc1a  22438  ftc1lem4  22440  ftc2ditglem  22446  itgsubstlem  22449  ig1peu  22572  ig1pdvds  22577  taylfvallem1  22752  tayl0  22757  taylply2  22763  taylply  22764  dvtaylp  22765  dvntaylp  22766  dvntaylp0  22767  taylthlem1  22768  ulmdvlem1  22795  ulmdvlem3  22797  psercn  22821  pserdvlem2  22823  abelth  22836  xrlimcnp  23298  wilthlem2  23343  sqff1o  23456  chtublem  23486  pntlemq  23786  pntlemf  23790  tglineintmo  24022  ttgcontlem1  24188  ghsubgolemOLD  25372  shintcli  26247  shub1  26300  mdslmd1lem1  27244  mdexchi  27254  chirredlem1  27309  mdsymlem5  27326  sumdmdii  27334  sumdmdlem2  27338  xrsupssd  27579  xrge0infssd  27581  xrge0tsmsd  27775  locfinreflem  27843  cmpcref  27853  pnfneige0  27933  insiga  28137  sssigagen2  28146  dya2iocnei  28253  omsmon  28267  lgamucov  28580  erdszelem7  28641  erdszelem8  28642  erdsze2lem1  28647  conpcon  28680  cvmliftmolem1  28726  cvmlift2lem1  28747  cvmlift2lem9  28756  cvmlift2lem10  28757  cvmlift3lem6  28769  cvmlift3lem7  28770  ss2mcls  28928  rtrclreclem.min  29070  dftrpred3g  29316  nofulllem3  29464  ontgval  29896  opnmbllem0  30050  ftc1anclem7  30096  ftc1anclem8  30097  ftc1anc  30098  neibastop2lem  30178  fnemeet2  30185  fnejoin1  30186  sstotbnd2  30270  heiborlem1  30307  heiborlem8  30314  intidl  30426  elrfi  30626  ismrcd1  30630  istopclsd  30632  mrefg2  30639  aomclem2  31001  aomclem6  31005  hbtlem6  31078  hbt  31079  limccog  31626  limclner  31657  cncfmptssg  31672  cncfuni  31689  icccncfext  31690  dvresntr  31713  dvmptresicc  31716  dvbdfbdioolem1  31725  dvdmsscn  31733  dvnxpaek  31739  dvnprodlem2  31744  stoweidlem59  31841  fourierdlem20  31909  fourierdlem42  31931  fourierdlem48  31937  fourierdlem49  31938  fourierdlem52  31941  fourierdlem58  31947  fourierdlem64  31953  fourierdlem73  31962  fourierdlem76  31965  fourierdlem80  31969  fourierdlem84  31973  fourierdlem93  31982  fourierdlem103  31992  fourierdlem104  31993  fourierdlem113  32002  etransclem18  32035  subsubmgm  32485  bnj906  33988  bnj1020  34021  bnj1137  34051  bnj1408  34092  bnj1452  34108  lsmsat  34733  lssats  34737  lpssat  34738  lssatle  34740  lssat  34741  lsatcvatlem  34774  paddss12  35543  paddasslem17  35560  pmodlem1  35570  pmod1i  35572  pmodl42N  35575  elpcliN  35617  pclfinN  35624  polcon3N  35641  polcon2N  35643  paddunN  35651  pclfinclN  35674  poml5N  35678  osumcllem1N  35680  osumcllem2N  35681  osumcllem3N  35682  pl42lem2N  35704  pl42lem4N  35706  cdlemn5pre  36927  dihord1  36945  dihord2a  36946  dihord2b  36947  dihord5b  36986  dochss  37092  dochdmj1  37117  djhsumss  37134  djhunssN  37136  dochexmidlem2  37188  lclkrslem1  37264  lclkrslem2  37265  lcfrlem2  37270  trrelssd  37777  imo72b2lem0  37982  imo72b2lem2  37984  imo72b2lem1  37988  imo72b2  37993
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