Theorem eqsstrdi 3953

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

This proof depends on syntax axioms:   → wi 4   = wceq 1569   ⊆ wss 3896

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-9 2154  ax-ext 2732

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

This theorem is used by:  eqsstrrdi  3954  eqimssd  3965  dmxpss  6165  dmsnopss  6218  iotassuni  6517  fvmptss  7011  fvmptss2  7025  funressn  7168  riotassuni  7421  ordsuci  7826  frxp  8144  suppssdm  8201  suppun  8208  suppss  8218  suppssov1  8221  suppssov2  8222  suppss2  8224  suppssfv  8226  oawordeulem  8569  omwordri  8587  oewordri  8608  mapssfset  8880  fodomr  9154  fodomfir  9326  fipwuni  9425  fipwss  9428  ordtypelem6  9524  inf3lemd  9635  cantnfle  9679  cantnflem2  9698  ttrclselem1  9733  setrec2fun  9980  en2other2  10095  ackbij1lem15  10318  ackbij2lem3  10325  cfub  10333  cflecard  10337  cfle  10338  fin23lem13  10417  fin23lem29  10426  compsscnvlem  10455  itunitc1  10505  fpwwe2lem11  10733  grur1a  10911  uzssz  12993  fsuppmapnn0fiublem  14140  fsuppmapnn0fiub  14141  swrdlend  14811  repswswrd  14943  cshimadifsn  14988  xptrrel  15142  relexpnndm  15203  relexpdmd  15206  relexprnd  15210  relexpfldd  15212  rtrclreclem4  15223  limsupgle  15653  isercolllem2  15842  isercolllem3  15843  isercoll  15844  fsumss  15900  sadcaddlem  16636  sadadd2lem  16638  sadadd3  16640  sadcl  16641  sadaddlem  16645  sadasslem  16649  sadeq  16651  smupvallem  16662  smucl  16663  prmreclem4  17106  prmreclem5  17107  1arith  17114  vdwmc2  17166  vdwlem13  17180  ramz2  17211  strfvss  17374  ressbasssg  17424  ressbasssOLD  17427  prdsless  17643  sectss  17936  invss  17945  fullfunc  18092  fthfunc  18093  catccatid  18290  resscatc  18293  catcisolem  18294  catciso  18295  yoniso  18468  gsumpropd2lem  18877  cntzrcl  19550  cntzssv  19551  gsumzmhm  20160  ablfaclem3  20312  rnghmresfn  20880  dfrngc2  20889  rnghmsscmap2  20890  rnghmsscmap  20891  funcrngcsetc  20901  rhmresfn  20909  dfringc2  20918  rhmsscmap2  20919  rhmsscmap  20920  rhmsscrnghm  20926  funcringcsetc  20935  rngcrescrhm  20945  rhmsubclem1  20946  rhmsubclem4  20949  lmhmlsp  21333  evpmss  21901  cssss  22000  frlmplusgval  22079  frlmvscafval  22081  uvcresum  22108  resspsrbas  22290  resspsrvsca  22293  subrgpsr  22294  mplsubglem  22315  ressmplbas  22345  subrgmpl  22349  mplsubrgcl  22350  opsrtoslem2  22374  mpfrcl  22403  ressply1bas  22555  ressply1evl  22697  evls1addd  22698  evls1muld  22699  evls1vsca  22700  evls1fvcl  22702  evls1maprhm  22703  scmatlss  22849  cpmatsubgpmat  23047  toponsspwpw  23249  basdif0  23280  ntrss2  23384  ordtbas2  23518  ordtbas  23519  cncls  23601  cmpfi  23735  comppfsc  23860  kgentopon  23866  ptpjpre1  23899  xkoccn  23947  prdstopn  23956  uzfbas  24226  utoptop  24562  utopbas  24563  setsmstopn  24806  restmetu  24898  tngtopn  24978  iccntr  25150  metdstri  25180  pi1xfrcnvlem  25386  cphsubrglem  25507  tcphcph  25567  rrxnm  25721  rrxbasefi  25740  ovolshftlem1  25839  ovolshft  25841  ovolscalem1  25843  ovolscalem2  25844  ovolsca  25845  uniioombllem2  25913  uniioombllem3a  25914  uniioombllem3  25915  uniioombllem4  25916  uniioombllem6  25918  itgioo  26145  limcnlp  26207  dvbsss  26231  dvcnvrelem1  26346  dvfsumle  26350  dvfsumabs  26352  pserdv  26765  rlimcnp2  27303  fsumharmonic  27348  chpval2  27554  bday0b  28208  madef  28231  madess  28261  oldssmade  28262  oldss  28265  n0bday  28747  bdayn0p1  28764  bdaypw2n0bndlem  28858  bdaypw2n0bnd  28859  tglnssp  29024  perpln1  29194  perpln2  29195  cgrabasimass  29387  uhgrspansubgr  29881  clwwlknclwwlkdifnum  30580  ocsh  31894  shsss  31924  speccl  32510  elnlfn  32539  pj3i  32819  sumdmdlem2  33030  fcoinver  33249  ffsrn  33370  ssnnssfz  33429  pfxrn2  33557  ccatws1f1o  33564  cycpmrn  33754  cycpmconjslem2  33766  fxpss  33777  inftmrel  33791  ressply1mon1p  34150  ressply1invg  34151  evls1subd  34154  esplyind  34257  algextdeglem7  34405  algextdeglem8  34406  smatrcl  34478  metidss  34573  fsumcvg4  34632  dya2iocuni  34965  carsgcl  34986  breprexplema  35309  bnj1143  35470  bnj1262  35490  bnj517  35565  kur14lem1  36061  cvmliftmolem2  36137  cvmliftlem15  36153  mrsubrn  36368  msubrn  36384  dfttc2g  37390  poimirlem30  38677  mblfinlem2  38685  sdclem2  38785  sstotbnd2  38817  isbnd3  38827  lkrlss  40261  pmapssat  40925  diass  42208  diaintclN  42224  dia2dimlem13  42242  dibintclN  42333  lcfrlem25  42733  lcdvbasess  42760  mapdin  42828  diophin  43892  rmxyelqirr  44026  itgocn  44275  oaabsb  44405  oege1  44417  oege2  44418  oacl2g  44441  tfsconcatb0  44455  ofoafg  44465  ofoaf  44466  fpwfvss  44522  relexp0a  44825  frege131d  44873  fsovrfovd  45118  clsk1indlem2  45151  clsk1indlem3  45152  mnuprd  45369  unirestss  46247  founiiun0  46313  fsumsupp0  46698  limsupequzlem  46840  dvnprodlem1  47064  ibliooicc  47089  stoweidlem34  47152  stoweidlem59  47177  etransclem24  47376  caratheodory  47646  ovnhoilem1  47719  hspdifhsp  47734  sssmf  47856  smfaddlem2  47882  smflimlem1  47889  smflimlem2  47890  smfmullem4  47912  smfsuplem1  47929  fcoreslem4  48244  fcoresf1  48247  fcoresfo  48249  dfnbgrss  49058  dfnbgrss2  49065  isubgrsubgr  49075  rngchomrnghmresALTV  49484  rngcrescrhmALTV  49485  rhmsubcALTVlem1  49486  funcringcsetcALTV2lem9  49503  ssnn0ssfz  49569  isclatd  50205  nelsubclem  50289  setrec2mpt  50973