Theorem eqsstrdi 3975

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

Step	Hyp	Ref	Expression
1		eqsstrdi.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		eqsstrdi.2	. . 3 ⊢ 𝐵 ⊆ 𝐶
3	2	a1i 11	. 2 ⊢ (𝜑 → 𝐵 ⊆ 𝐶)
4	1, 3	eqsstrd 3965	1 ⊢ (𝜑 → 𝐴 ⊆ 𝐶)

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ⊆ wss 3899

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2752  df-ss 3916

This theorem is used by:  eqsstrrdi  3976  eqimssd  3987  dmxpss  6164  dmsnopss  6210  iotassuni  6508  fvmptss  7000  fvmptss2  7014  funressn  7157  riotassuni  7411  ordsuci  7808  frxp  8125  suppssdm  8176  suppun  8183  suppss  8193  suppssov1  8196  suppssov2  8197  suppss2  8199  suppssfv  8201  oawordeulem  8544  omwordri  8562  oewordri  8583  mapssfset  8855  fodomr  9129  fodomfir  9300  fipwuni  9399  fipwss  9402  ordtypelem6  9498  inf3lemd  9609  cantnfle  9653  cantnflem2  9672  ttrclselem1  9707  en2other2  10015  ackbij1lem15  10238  ackbij2lem3  10245  cfub  10253  cflecard  10257  cfle  10258  fin23lem13  10337  fin23lem29  10346  compsscnvlem  10375  itunitc1  10425  fpwwe2lem11  10653  grur1a  10831  uzssz  12911  fsuppmapnn0fiublem  14057  fsuppmapnn0fiub  14058  swrdlend  14726  repswswrd  14858  cshimadifsn  14903  xptrrel  15056  relexpnndm  15117  relexpdmd  15120  relexprnd  15124  relexpfldd  15126  rtrclreclem4  15137  limsupgle  15567  isercolllem2  15756  isercolllem3  15757  isercoll  15758  fsumss  15814  sadcaddlem  16550  sadadd2lem  16552  sadadd3  16554  sadcl  16555  sadaddlem  16559  sadasslem  16563  sadeq  16565  smupvallem  16576  smucl  16577  prmreclem4  17014  prmreclem5  17015  1arith  17022  vdwmc2  17074  vdwlem13  17088  ramz2  17119  strfvss  17282  ressbasssg  17332  ressbasssOLD  17335  prdsless  17551  sectss  17844  invss  17853  fullfunc  18000  fthfunc  18001  catccatid  18198  resscatc  18201  catcisolem  18202  catciso  18203  yoniso  18376  gsumpropd2lem  18784  cntzrcl  19457  cntzssv  19458  gsumzmhm  20067  ablfaclem3  20219  rnghmresfn  20784  dfrngc2  20793  rnghmsscmap2  20794  rnghmsscmap  20795  funcrngcsetc  20805  rhmresfn  20813  dfringc2  20822  rhmsscmap2  20823  rhmsscmap  20824  rhmsscrnghm  20830  funcringcsetc  20839  rngcrescrhm  20849  rhmsubclem1  20850  rhmsubclem4  20853  lmhmlsp  21236  evpmss  21802  cssss  21901  frlmplusgval  21980  frlmvscafval  21982  uvcresum  22009  resspsrbas  22191  resspsrvsca  22194  subrgpsr  22195  mplsubglem  22216  ressmplbas  22246  subrgmpl  22250  mplsubrgcl  22251  opsrtoslem2  22275  mpfrcl  22304  ressply1bas  22456  ressply1evl  22598  evls1addd  22599  evls1muld  22600  evls1vsca  22601  evls1fvcl  22603  evls1maprhm  22604  scmatlss  22750  cpmatsubgpmat  22948  toponsspwpw  23150  basdif0  23181  ntrss2  23285  ordtbas2  23419  ordtbas  23420  cncls  23502  cmpfi  23636  comppfsc  23761  kgentopon  23767  ptpjpre1  23800  xkoccn  23848  prdstopn  23857  uzfbas  24127  utoptop  24463  utopbas  24464  setsmstopn  24707  restmetu  24799  tngtopn  24879  iccntr  25051  metdstri  25081  pi1xfrcnvlem  25287  cphsubrglem  25408  tcphcph  25468  rrxnm  25622  rrxbasefi  25641  ovolshftlem1  25740  ovolshft  25742  ovolscalem1  25744  ovolscalem2  25745  ovolsca  25746  uniioombllem2  25814  uniioombllem3a  25815  uniioombllem3  25816  uniioombllem4  25817  uniioombllem6  25819  itgioo  26046  limcnlp  26108  dvbsss  26132  dvcnvrelem1  26247  dvfsumle  26251  dvfsumabs  26253  pserdv  26668  rlimcnp2  27206  fsumharmonic  27251  chpval2  27457  bday0b  28081  madef  28104  madess  28134  oldssmade  28135  oldss  28138  n0bday  28620  bdayn0p1  28637  bdaypw2n0bndlem  28731  bdaypw2n0bnd  28732  tglnssp  28897  perpln1  29067  perpln2  29068  cgrabasimass  29260  uhgrspansubgr  29754  clwwlknclwwlkdifnum  30453  ocsh  31767  shsss  31797  speccl  32383  elnlfn  32412  pj3i  32692  sumdmdlem2  32903  fcoinver  33080  ffsrn  33202  ssnnssfz  33261  pfxrn2  33389  ccatws1f1o  33396  cycpmrn  33586  cycpmconjslem2  33598  fxpss  33609  inftmrel  33623  ressply1mon1p  33981  ressply1invg  33982  evls1subd  33985  esplyind  34088  algextdeglem7  34236  algextdeglem8  34237  smatrcl  34309  metidss  34404  fsumcvg4  34463  dya2iocuni  34797  carsgcl  34818  breprexplema  35141  bnj1143  35302  bnj1262  35322  bnj517  35397  kur14lem1  35788  cvmliftmolem2  35864  cvmliftlem15  35880  mrsubrn  36095  msubrn  36111  dfttc2g  37128  poimirlem30  38402  mblfinlem2  38410  sdclem2  38495  sstotbnd2  38527  isbnd3  38537  lkrlss  39971  pmapssat  40635  diass  41918  diaintclN  41934  dia2dimlem13  41952  dibintclN  42043  lcfrlem25  42443  lcdvbasess  42470  mapdin  42538  diophin  43620  rmxyelqirr  43754  itgocn  44008  oaabsb  44138  oege1  44150  oege2  44151  oacl2g  44174  tfsconcatb0  44188  ofoafg  44198  ofoaf  44199  fpwfvss  44255  relexp0a  44559  frege131d  44607  fsovrfovd  44852  clsk1indlem2  44885  clsk1indlem3  44886  mnuprd  45103  unirestss  45959  founiiun0  46025  fsumsupp0  46411  limsupequzlem  46553  dvnprodlem1  46777  ibliooicc  46802  stoweidlem34  46865  stoweidlem59  46890  etransclem24  47089  caratheodory  47359  ovnhoilem1  47432  hspdifhsp  47447  sssmf  47569  smfaddlem2  47595  smflimlem1  47602  smflimlem2  47603  smfmullem4  47625  smfsuplem1  47642  fcoreslem4  47957  fcoresf1  47960  fcoresfo  47962  dfnbgrss  48771  dfnbgrss2  48778  isubgrsubgr  48788  rngchomrnghmresALTV  49197  rngcrescrhmALTV  49198  rhmsubcALTVlem1  49199  funcringcsetcALTV2lem9  49216  ssnn0ssfz  49282  isclatd  49912  nelsubclem  49996  setrec2fun  50621  setrec2mpt  50626