Theorem eqsstrdi 4028

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 4018	1 ⊢ (𝜑 → 𝐴 ⊆ 𝐶)

Syntax hints:   → wi 4   = wceq 1540   ⊆ wss 3951

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2729  df-ss 3968

This theorem is referenced by:  eqsstrrdi  4029  eqimssd  4040  dmxpss  6191  dmsnopss  6234  iotassuni  6533  iotassuniOLD  6540  fvmptss  7028  fvmptss2  7042  funressn  7179  riotassuni  7428  ordsuci  7828  frxp  8151  suppssdm  8202  suppun  8209  suppss  8219  suppssov1  8222  suppssov2  8223  suppss2  8225  suppssfv  8227  wfrlem15OLD  8363  oawordeulem  8592  omwordri  8610  oewordri  8630  mapssfset  8891  fodomr  9168  fodomfir  9368  fipwuni  9466  fipwss  9469  ordtypelem6  9563  inf3lemd  9667  cantnfle  9711  cantnflem2  9730  ttrclselem1  9765  en2other2  10049  ackbij1lem15  10273  ackbij2lem3  10280  cfub  10289  cflecard  10293  cfle  10294  fin23lem13  10372  fin23lem29  10381  compsscnvlem  10410  itunitc1  10460  fpwwe2lem11  10681  grur1a  10859  uzssz  12899  fsuppmapnn0fiublem  14031  fsuppmapnn0fiub  14032  swrdlend  14691  repswswrd  14822  cshimadifsn  14868  xptrrel  15019  relexpnndm  15080  relexpdmd  15083  relexprnd  15087  relexpfldd  15089  rtrclreclem4  15100  limsupgle  15513  isercolllem2  15702  isercolllem3  15703  isercoll  15704  fsumss  15761  sadcaddlem  16494  sadadd2lem  16496  sadadd3  16498  sadcl  16499  sadaddlem  16503  sadasslem  16507  sadeq  16509  smupvallem  16520  smucl  16521  prmreclem4  16957  prmreclem5  16958  1arith  16965  vdwmc2  17017  vdwlem13  17031  ramz2  17062  strfvss  17224  ressbasssg  17282  ressbasssOLD  17285  prdsless  17508  sectss  17796  invss  17805  fullfunc  17953  fthfunc  17954  catccatid  18151  resscatc  18154  catcisolem  18155  catciso  18156  yoniso  18330  gsumpropd2lem  18692  cntzrcl  19345  cntzssv  19346  gsumzmhm  19955  ablfaclem3  20107  rnghmresfn  20619  dfrngc2  20628  rnghmsscmap2  20629  rnghmsscmap  20630  funcrngcsetc  20640  rhmresfn  20648  dfringc2  20657  rhmsscmap2  20658  rhmsscmap  20659  rhmsscrnghm  20665  funcringcsetc  20674  rngcrescrhm  20684  rhmsubclem1  20685  rhmsubclem4  20688  lmhmlsp  21048  evpmss  21604  cssss  21703  frlmplusgval  21784  frlmvscafval  21786  uvcresum  21813  resspsrbas  21994  resspsrvsca  21997  subrgpsr  21998  mplsubglem  22019  ressmplbas  22046  subrgmpl  22050  opsrtoslem2  22080  mpfrcl  22109  ressply1bas  22230  ressply1evl  22374  evls1addd  22375  evls1muld  22376  evls1vsca  22377  evls1fvcl  22379  evls1maprhm  22380  scmatlss  22531  cpmatsubgpmat  22726  toponsspwpw  22928  basdif0  22960  ntrss2  23065  ordtbas2  23199  ordtbas  23200  cncls  23282  cmpfi  23416  comppfsc  23540  kgentopon  23546  ptpjpre1  23579  xkoccn  23627  prdstopn  23636  uzfbas  23906  utoptop  24243  utopbas  24244  setsmstopn  24490  restmetu  24583  tngtopn  24671  iccntr  24843  metdstri  24873  pi1xfrcnvlem  25089  cphsubrglem  25211  tcphcph  25271  rrxnm  25425  rrxbasefi  25444  ovolshftlem1  25544  ovolshft  25546  ovolscalem1  25548  ovolscalem2  25549  ovolsca  25550  uniioombllem2  25618  uniioombllem3a  25619  uniioombllem3  25620  uniioombllem4  25621  uniioombllem6  25623  itgioo  25851  limcnlp  25913  dvbsss  25937  dvcnvrelem1  26056  dvfsumle  26060  dvfsumleOLD  26061  dvfsumabs  26063  pserdv  26473  rlimcnp2  27009  fsumharmonic  27055  chpval2  27262  bday0b  27875  madef  27895  madess  27915  oldssmade  27916  n0sbday  28354  tglnssp  28560  perpln1  28718  perpln2  28719  uhgrspansubgr  29308  clwwlknclwwlkdifnum  29999  ocsh  31302  shsss  31332  speccl  31918  elnlfn  31947  pj3i  32227  sumdmdlem2  32438  fcoinver  32617  ffsrn  32740  ssnnssfz  32789  pfxrn2  32924  ccatws1f1o  32936  cycpmrn  33163  cycpmconjslem2  33175  inftmrel  33187  ressply1mon1p  33593  ressply1invg  33594  evls1subd  33597  algextdeglem7  33764  algextdeglem8  33765  smatrcl  33795  metidss  33890  fsumcvg4  33949  dya2iocuni  34285  carsgcl  34306  breprexplema  34645  bnj1143  34804  bnj1262  34824  bnj517  34899  kur14lem1  35211  cvmliftmolem2  35287  cvmliftlem15  35303  mrsubrn  35518  msubrn  35534  poimirlem30  37657  mblfinlem2  37665  sdclem2  37749  sstotbnd2  37781  isbnd3  37791  lkrlss  39096  pmapssat  39761  diass  41044  diaintclN  41060  dia2dimlem13  41078  dibintclN  41169  lcfrlem25  41569  lcdvbasess  41596  mapdin  41664  mplsubrgcl  42558  diophin  42783  rmxyelqirr  42921  itgocn  43176  oaabsb  43307  oege1  43319  oege2  43320  oacl2g  43343  tfsconcatb0  43357  ofoafg  43367  ofoaf  43368  fpwfvss  43425  relexp0a  43729  frege131d  43777  fsovrfovd  44022  clsk1indlem2  44055  clsk1indlem3  44056  mnuprd  44295  unirestss  45129  founiiun0  45195  fsumsupp0  45593  limsupequzlem  45737  dvnprodlem1  45961  ibliooicc  45986  stoweidlem34  46049  stoweidlem59  46074  etransclem24  46273  caratheodory  46543  ovnhoilem1  46616  hspdifhsp  46631  smfaddlem2  46779  smflimlem1  46786  smflimlem2  46787  smfmullem4  46809  smfsuplem1  46826  fcoreslem4  47078  fcoresf1  47081  fcoresfo  47083  dfnbgrss  47838  dfnbgrss2  47845  isubgrsubgr  47855  rngchomrnghmresALTV  48195  rngcrescrhmALTV  48196  rhmsubcALTVlem1  48197  funcringcsetcALTV2lem9  48214  ssnn0ssfz  48265  isclatd  48872  setrec2fun  49211  setrec2mpt  49216