MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  eqsstrdi Structured version   Visualization version   GIF version

Theorem eqsstrdi 3996
Description: A chained subclass and equality deduction. (Contributed by Mario Carneiro, 2-Jan-2017.)
Hypotheses
Ref Expression
eqsstrdi.1 (𝜑𝐴 = 𝐵)
eqsstrdi.2 𝐵𝐶
Assertion
Ref Expression
eqsstrdi (𝜑𝐴𝐶)

Proof of Theorem eqsstrdi
StepHypRef Expression
1 eqsstrdi.1 . 2 (𝜑𝐴 = 𝐵)
2 eqsstrdi.2 . . 3 𝐵𝐶
32a1i 11 . 2 (𝜑𝐵𝐶)
41, 3eqsstrd 3980 1 (𝜑𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1541  wss 3908
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2708
This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2715  df-cleq 2729  df-clel 2815  df-v 3445  df-in 3915  df-ss 3925
This theorem is referenced by:  eqsstrrdi  3997  dmxpss  6119  dmsnopss  6162  iotassuni  6463  iotassuniOLD  6470  fvmptss  6955  fvmptss2  6968  fimacnvOLD  7016  funressn  7099  riotassuni  7346  ordsuci  7733  frxp  8046  suppssdm  8075  suppun  8082  suppss  8092  suppssOLD  8093  suppssov1  8096  suppss2  8098  suppssfv  8100  wfrlem15OLD  8236  oawordeulem  8468  omwordri  8486  oewordri  8506  mapssfset  8722  fodomr  9005  fipwuni  9295  fipwss  9298  ordtypelem6  9392  inf3lemd  9496  cantnfle  9540  cantnflem2  9559  ttrclselem1  9594  en2other2  9878  ackbij1lem15  10103  ackbij2lem3  10110  cfub  10118  cflecard  10122  cfle  10123  fin23lem13  10201  fin23lem29  10210  compsscnvlem  10239  itunitc1  10289  fpwwe2lem11  10510  grur1a  10688  uzssz  12716  fsuppmapnn0fiublem  13823  fsuppmapnn0fiub  13824  swrdlend  14472  repswswrd  14603  cshimadifsn  14649  xptrrel  14798  relexpnndm  14859  relexpdmd  14862  relexprnd  14866  relexpfldd  14868  rtrclreclem4  14879  limsupgle  15293  isercolllem2  15484  isercolllem3  15485  isercoll  15486  fsumss  15544  sadcaddlem  16271  sadadd2lem  16273  sadadd3  16275  sadcl  16276  sadaddlem  16280  sadasslem  16284  sadeq  16286  smupvallem  16297  smucl  16298  prmreclem4  16725  prmreclem5  16726  1arith  16733  vdwmc2  16785  vdwlem13  16799  ramz2  16830  strfvss  16993  ressbasss  17055  prdsless  17279  sectss  17569  invss  17578  fullfunc  17727  fthfunc  17728  catccatid  17926  resscatc  17929  catcisolem  17930  catciso  17931  yoniso  18108  gsumpropd2lem  18468  cntzrcl  19039  cntzssv  19040  gsumzmhm  19643  ablfaclem3  19795  lmhmlsp  20433  evpmss  20913  cssss  21012  frlmplusgval  21093  frlmvscafval  21095  uvcresum  21122  resspsrbas  21306  resspsrvsca  21309  subrgpsr  21310  mplsubglem  21327  ressmplbas  21351  subrgmpl  21355  mpfrcl  21417  ressply1bas  21522  scmatlss  21796  cpmatsubgpmat  21991  toponsspwpw  22193  basdif0  22225  ntrss2  22330  ordtbas2  22464  ordtbas  22465  cncls  22547  cmpfi  22681  comppfsc  22805  kgentopon  22811  ptpjpre1  22844  xkoccn  22892  prdstopn  22901  uzfbas  23171  utoptop  23508  utopbas  23509  setsmstopn  23755  restmetu  23848  tngtopn  23936  iccntr  24106  metdstri  24136  pi1xfrcnvlem  24341  cphsubrglem  24463  tcphcph  24523  rrxnm  24677  rrxbasefi  24696  ovolshftlem1  24795  ovolshft  24797  ovolscalem1  24799  ovolscalem2  24800  ovolsca  24801  uniioombllem2  24869  uniioombllem3a  24870  uniioombllem3  24871  uniioombllem4  24872  uniioombllem6  24874  itgioo  25102  limcnlp  25164  dvbsss  25188  dvcnvrelem1  25303  dvfsumle  25307  dvfsumabs  25309  pserdv  25710  rlimcnp2  26238  fsumharmonic  26283  chpval2  26488  bday0b  27091  madef  27107  madess  27126  oldssmade  27127  tglnssp  27292  perpln1  27450  perpln2  27451  uhgrspansubgr  28037  clwwlknclwwlkdifnum  28722  ocsh  30023  shsss  30053  speccl  30639  elnlfn  30668  pj3i  30948  sumdmdlem2  31159  fcoinver  31322  ffsrn  31440  ssnnssfz  31484  pfxrn2  31590  cycpmrn  31786  cycpmconjslem2  31798  inftmrel  31810  ressply1evl  32059  evls1muld  32060  ressply1mon1p  32064  minplyeulem  32146  smatrcl  32150  metidss  32245  fsumcvg4  32304  dya2iocuni  32656  carsgcl  32677  breprexplema  33016  bnj1143  33175  bnj1262  33195  bnj517  33270  kur14lem1  33573  cvmliftmolem2  33649  cvmliftlem15  33665  mrsubrn  33880  msubrn  33896  poimirlem30  36003  mblfinlem2  36011  sdclem2  36096  sstotbnd2  36128  isbnd3  36138  lkrlss  37452  pmapssat  38117  diass  39400  diaintclN  39416  dia2dimlem13  39434  dibintclN  39525  lcfrlem25  39925  lcdvbasess  39952  mapdin  40020  eqimssd  40530  ressbasssg  40562  diophin  40960  rmxyelqirr  41098  itgocn  41356  oacl2g  41421  ofoafg  41425  ofoaf  41426  fpwfvss  41446  relexp0a  41750  frege131d  41798  fsovrfovd  42043  clsk1indlem2  42078  clsk1indlem3  42079  mnuprd  42320  unirestss  43098  founiiun0  43166  fsumsupp0  43572  limsupequzlem  43716  ibliooicc  43965  stoweidlem34  44028  stoweidlem59  44053  etransclem24  44252  caratheodory  44522  ovnhoilem1  44595  hspdifhsp  44610  smfaddlem2  44758  smflimlem1  44765  smflimlem2  44766  smfmullem4  44788  smfsuplem1  44805  fcoreslem4  45049  fcoresf1  45052  fcoresfo  45054  rnghmresfn  46010  dfrngc2  46019  rnghmsscmap2  46020  rnghmsscmap  46021  rngchomrnghmresALTV  46043  funcrngcsetc  46045  rhmresfn  46056  dfringc2  46065  rhmsscmap2  46066  rhmsscmap  46067  rhmsscrnghm  46073  funcringcsetc  46082  funcringcsetcALTV2lem9  46091  rngcrescrhm  46132  rhmsubclem1  46133  rhmsubclem4  46136  rngcrescrhmALTV  46150  rhmsubcALTVlem1  46151  ssnn0ssfz  46174  isclatd  46757  setrec2fun  46886
  Copyright terms: Public domain W3C validator