Theorem eqsstrdi 4049

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

Syntax hints:   → wi 4   = wceq 1536   ⊆ wss 3962

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1776  df-cleq 2726  df-ss 3979

This theorem is referenced by:  eqsstrrdi  4050  eqimssd  4051  dmxpss  6192  dmsnopss  6235  iotassuni  6534  iotassuniOLD  6541  fvmptss  7027  fvmptss2  7041  funressn  7178  riotassuni  7427  ordsuci  7827  frxp  8149  suppssdm  8200  suppun  8207  suppss  8217  suppssov1  8220  suppssov2  8221  suppss2  8223  suppssfv  8225  wfrlem15OLD  8361  oawordeulem  8590  omwordri  8608  oewordri  8628  mapssfset  8889  fodomr  9166  fodomfir  9365  fipwuni  9463  fipwss  9466  ordtypelem6  9560  inf3lemd  9664  cantnfle  9708  cantnflem2  9727  ttrclselem1  9762  en2other2  10046  ackbij1lem15  10270  ackbij2lem3  10277  cfub  10286  cflecard  10290  cfle  10291  fin23lem13  10369  fin23lem29  10378  compsscnvlem  10407  itunitc1  10457  fpwwe2lem11  10678  grur1a  10856  uzssz  12896  fsuppmapnn0fiublem  14027  fsuppmapnn0fiub  14028  swrdlend  14687  repswswrd  14818  cshimadifsn  14864  xptrrel  15015  relexpnndm  15076  relexpdmd  15079  relexprnd  15083  relexpfldd  15085  rtrclreclem4  15096  limsupgle  15509  isercolllem2  15698  isercolllem3  15699  isercoll  15700  fsumss  15757  sadcaddlem  16490  sadadd2lem  16492  sadadd3  16494  sadcl  16495  sadaddlem  16499  sadasslem  16503  sadeq  16505  smupvallem  16516  smucl  16517  prmreclem4  16952  prmreclem5  16953  1arith  16960  vdwmc2  17012  vdwlem13  17026  ramz2  17057  strfvss  17220  ressbasssg  17281  ressbasssOLD  17284  prdsless  17509  sectss  17799  invss  17808  fullfunc  17959  fthfunc  17960  catccatid  18159  resscatc  18162  catcisolem  18163  catciso  18164  yoniso  18341  gsumpropd2lem  18704  cntzrcl  19357  cntzssv  19358  gsumzmhm  19969  ablfaclem3  20121  rnghmresfn  20635  dfrngc2  20644  rnghmsscmap2  20645  rnghmsscmap  20646  funcrngcsetc  20656  rhmresfn  20664  dfringc2  20673  rhmsscmap2  20674  rhmsscmap  20675  rhmsscrnghm  20681  funcringcsetc  20690  rngcrescrhm  20700  rhmsubclem1  20701  rhmsubclem4  20704  lmhmlsp  21065  evpmss  21621  cssss  21720  frlmplusgval  21801  frlmvscafval  21803  uvcresum  21830  resspsrbas  22011  resspsrvsca  22014  subrgpsr  22015  mplsubglem  22036  ressmplbas  22063  subrgmpl  22067  opsrtoslem2  22097  mpfrcl  22126  ressply1bas  22245  ressply1evl  22389  evls1addd  22390  evls1muld  22391  evls1vsca  22392  evls1fvcl  22394  evls1maprhm  22395  scmatlss  22546  cpmatsubgpmat  22741  toponsspwpw  22943  basdif0  22975  ntrss2  23080  ordtbas2  23214  ordtbas  23215  cncls  23297  cmpfi  23431  comppfsc  23555  kgentopon  23561  ptpjpre1  23594  xkoccn  23642  prdstopn  23651  uzfbas  23921  utoptop  24258  utopbas  24259  setsmstopn  24505  restmetu  24598  tngtopn  24686  iccntr  24856  metdstri  24886  pi1xfrcnvlem  25102  cphsubrglem  25224  tcphcph  25284  rrxnm  25438  rrxbasefi  25457  ovolshftlem1  25557  ovolshft  25559  ovolscalem1  25561  ovolscalem2  25562  ovolsca  25563  uniioombllem2  25631  uniioombllem3a  25632  uniioombllem3  25633  uniioombllem4  25634  uniioombllem6  25636  itgioo  25865  limcnlp  25927  dvbsss  25951  dvcnvrelem1  26070  dvfsumle  26074  dvfsumleOLD  26075  dvfsumabs  26077  pserdv  26487  rlimcnp2  27023  fsumharmonic  27069  chpval2  27276  bday0b  27889  madef  27909  madess  27929  oldssmade  27930  n0sbday  28368  tglnssp  28574  perpln1  28732  perpln2  28733  uhgrspansubgr  29322  clwwlknclwwlkdifnum  30008  ocsh  31311  shsss  31341  speccl  31927  elnlfn  31956  pj3i  32236  sumdmdlem2  32447  fcoinver  32623  ffsrn  32746  ssnnssfz  32795  pfxrn2  32908  ccatws1f1o  32920  cycpmrn  33145  cycpmconjslem2  33157  inftmrel  33169  ressply1mon1p  33572  ressply1invg  33573  evls1subd  33576  algextdeglem7  33728  algextdeglem8  33729  smatrcl  33756  metidss  33851  fsumcvg4  33910  dya2iocuni  34264  carsgcl  34285  breprexplema  34623  bnj1143  34782  bnj1262  34802  bnj517  34877  kur14lem1  35190  cvmliftmolem2  35266  cvmliftlem15  35282  mrsubrn  35497  msubrn  35513  poimirlem30  37636  mblfinlem2  37644  sdclem2  37728  sstotbnd2  37760  isbnd3  37770  lkrlss  39076  pmapssat  39741  diass  41024  diaintclN  41040  dia2dimlem13  41058  dibintclN  41149  lcfrlem25  41549  lcdvbasess  41576  mapdin  41644  mplsubrgcl  42534  diophin  42759  rmxyelqirr  42897  itgocn  43152  oaabsb  43283  oege1  43295  oege2  43296  oacl2g  43319  tfsconcatb0  43333  ofoafg  43343  ofoaf  43344  fpwfvss  43401  relexp0a  43705  frege131d  43753  fsovrfovd  43998  clsk1indlem2  44031  clsk1indlem3  44032  mnuprd  44271  unirestss  45063  founiiun0  45132  fsumsupp0  45533  limsupequzlem  45677  dvnprodlem1  45901  ibliooicc  45926  stoweidlem34  45989  stoweidlem59  46014  etransclem24  46213  caratheodory  46483  ovnhoilem1  46556  hspdifhsp  46571  smfaddlem2  46719  smflimlem1  46726  smflimlem2  46727  smfmullem4  46749  smfsuplem1  46766  fcoreslem4  47015  fcoresf1  47018  fcoresfo  47020  dfnbgrss  47775  dfnbgrss2  47782  isubgrsubgr  47792  rngchomrnghmresALTV  48122  rngcrescrhmALTV  48123  rhmsubcALTVlem1  48124  funcringcsetcALTV2lem9  48141  ssnn0ssfz  48193  isclatd  48771  setrec2fun  48922  setrec2mpt  48927