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

Theorem eqsstrdi 4021
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 4005 1 (𝜑𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1533  wss 3936
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2156  ax-12 2172  ax-ext 2793
This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-clab 2800  df-cleq 2814  df-clel 2893  df-in 3943  df-ss 3952
This theorem is referenced by:  eqsstrrdi  4022  dmxpss  6023  dmsnopss  6066  iotassuni  6329  fvmptss  6775  fvmptss2  6788  fimacnv  6834  funressn  6916  riotassuni  7148  frxp  7814  suppssdm  7837  suppun  7844  suppss  7854  suppssov1  7856  suppss2  7858  suppssfv  7860  wfrlem15  7963  oawordeulem  8174  omwordri  8192  oewordri  8212  fodomr  8662  fipwuni  8884  fipwss  8887  ordtypelem6  8981  inf3lemd  9084  cantnfle  9128  cantnflem2  9147  en2other2  9429  ackbij1lem15  9650  ackbij2lem3  9657  cfub  9665  cflecard  9669  cfle  9670  fin23lem13  9748  fin23lem29  9757  compsscnvlem  9786  itunitc1  9836  fpwwe2lem12  10057  grur1a  10235  uzssz  12258  fsuppmapnn0fiublem  13352  fsuppmapnn0fiub  13353  swrdlend  14009  repswswrd  14140  cshimadifsn  14185  xptrrel  14334  relexpnndm  14394  limsupgle  14828  isercolllem2  15016  isercolllem3  15017  isercoll  15018  fsumss  15076  sadcaddlem  15800  sadadd2lem  15802  sadadd3  15804  sadcl  15805  sadaddlem  15809  sadasslem  15813  sadeq  15815  smupvallem  15826  smucl  15827  prmreclem4  16249  prmreclem5  16250  1arith  16257  vdwmc2  16309  vdwlem13  16323  ramz2  16354  strfvss  16500  ressbasss  16550  prdsless  16730  sectss  17016  invss  17025  fullfunc  17170  fthfunc  17171  catccatid  17356  resscatc  17359  catcisolem  17360  catciso  17361  yoniso  17529  gsumpropd2lem  17883  cntzrcl  18451  cntzssv  18452  gsumzmhm  19051  ablfaclem3  19203  lmhmlsp  19815  resspsrbas  20189  resspsrvsca  20192  subrgpsr  20193  mplsubglem  20208  ressmplbas  20231  subrgmpl  20235  mpfrcl  20292  mhp0cl  20331  ressply1bas  20391  evpmss  20724  cssss  20823  frlmplusgval  20902  frlmvscafval  20904  uvcresum  20931  scmatlss  21128  cpmatsubgpmat  21322  toponsspwpw  21524  basdif0  21555  ntrss2  21659  ordtbas2  21793  ordtbas  21794  cncls  21876  cmpfi  22010  comppfsc  22134  kgentopon  22140  ptpjpre1  22173  xkoccn  22221  prdstopn  22230  uzfbas  22500  utoptop  22837  utopbas  22838  setsmstopn  23082  restmetu  23174  tngtopn  23253  iccntr  23423  metdstri  23453  pi1xfrcnvlem  23654  cphsubrglem  23775  tcphcph  23834  rrxnm  23988  rrxbasefi  24007  ovolshftlem1  24104  ovolshft  24106  ovolscalem1  24108  ovolscalem2  24109  ovolsca  24110  uniioombllem2  24178  uniioombllem3a  24179  uniioombllem3  24180  uniioombllem4  24181  uniioombllem6  24183  itgioo  24410  limcnlp  24470  dvbsss  24494  dvcnvrelem1  24608  dvfsumle  24612  dvfsumabs  24614  pserdv  25011  rlimcnp2  25538  fsumharmonic  25583  chpval2  25788  tglnssp  26332  perpln1  26490  perpln2  26491  uhgrspansubgr  27067  clwwlknclwwlkdifnum  27752  ocsh  29054  shsss  29084  speccl  29670  elnlfn  29699  pj3i  29979  sumdmdlem2  30190  fcoinver  30351  ffsrn  30459  ssnnssfz  30504  pfxrn2  30611  cycpmrn  30780  cycpmconjslem2  30792  inftmrel  30804  smatrcl  31056  metidss  31126  fsumcvg4  31188  dya2iocuni  31536  carsgcl  31557  breprexplema  31896  bnj1143  32057  bnj1262  32077  bnj517  32152  kur14lem1  32448  cvmliftmolem2  32524  cvmliftlem15  32540  mrsubrn  32755  msubrn  32771  trpredlem1  33061  poimirlem30  34916  mblfinlem2  34924  sdclem2  35011  sstotbnd2  35046  isbnd3  35056  lkrlss  36225  pmapssat  36889  diass  38172  diaintclN  38188  dia2dimlem13  38206  dibintclN  38297  lcfrlem25  38697  lcdvbasess  38724  mapdin  38792  diophin  39362  itgocn  39757  relexp0a  40054  frege131d  40102  fsovrfovd  40348  clsk1indlem2  40385  clsk1indlem3  40386  mnuprd  40605  unirestss  41383  founiiun0  41443  fsumsupp0  41851  limsupequzlem  41995  ibliooicc  42248  stoweidlem34  42312  stoweidlem59  42337  etransclem24  42536  caratheodory  42803  ovnhoilem1  42876  hspdifhsp  42891  smfaddlem2  43033  smflimlem1  43040  smflimlem2  43041  smfmullem4  43062  smfsuplem1  43078  rnghmresfn  44227  dfrngc2  44236  rnghmsscmap2  44237  rnghmsscmap  44238  rngchomrnghmresALTV  44260  funcrngcsetc  44262  rhmresfn  44273  dfringc2  44282  rhmsscmap2  44283  rhmsscmap  44284  rhmsscrnghm  44290  funcringcsetc  44299  funcringcsetcALTV2lem9  44308  rngcrescrhm  44349  rhmsubclem1  44350  rhmsubclem4  44353  rngcrescrhmALTV  44367  rhmsubcALTVlem1  44368  ssnn0ssfz  44390  setrec2fun  44788
  Copyright terms: Public domain W3C validator