Theorem eqsstrdi 4001

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

Syntax hints:   → wi 4   = wceq 1539   ⊆ wss 3924

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-9 2117  ax-ext 2706

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

This theorem is referenced by:  eqsstrrdi  4002  eqimssd  4013  dmxpss  6157  dmsnopss  6200  iotassuni  6499  iotassuniOLD  6506  fvmptss  6994  fvmptss2  7008  funressn  7145  riotassuni  7396  ordsuci  7796  frxp  8119  suppssdm  8170  suppun  8177  suppss  8187  suppssov1  8190  suppssov2  8191  suppss2  8193  suppssfv  8195  wfrlem15OLD  8331  oawordeulem  8560  omwordri  8578  oewordri  8598  mapssfset  8859  fodomr  9136  fodomfir  9334  fipwuni  9432  fipwss  9435  ordtypelem6  9529  inf3lemd  9633  cantnfle  9677  cantnflem2  9696  ttrclselem1  9731  en2other2  10015  ackbij1lem15  10239  ackbij2lem3  10246  cfub  10255  cflecard  10259  cfle  10260  fin23lem13  10338  fin23lem29  10347  compsscnvlem  10376  itunitc1  10426  fpwwe2lem11  10647  grur1a  10825  uzssz  12865  fsuppmapnn0fiublem  13997  fsuppmapnn0fiub  13998  swrdlend  14658  repswswrd  14789  cshimadifsn  14835  xptrrel  14986  relexpnndm  15047  relexpdmd  15050  relexprnd  15054  relexpfldd  15056  rtrclreclem4  15067  limsupgle  15480  isercolllem2  15669  isercolllem3  15670  isercoll  15671  fsumss  15728  sadcaddlem  16461  sadadd2lem  16463  sadadd3  16465  sadcl  16466  sadaddlem  16470  sadasslem  16474  sadeq  16476  smupvallem  16487  smucl  16488  prmreclem4  16924  prmreclem5  16925  1arith  16932  vdwmc2  16984  vdwlem13  16998  ramz2  17029  strfvss  17191  ressbasssg  17243  ressbasssOLD  17246  prdsless  17462  sectss  17750  invss  17759  fullfunc  17906  fthfunc  17907  catccatid  18104  resscatc  18107  catcisolem  18108  catciso  18109  yoniso  18282  gsumpropd2lem  18642  cntzrcl  19295  cntzssv  19296  gsumzmhm  19903  ablfaclem3  20055  rnghmresfn  20564  dfrngc2  20573  rnghmsscmap2  20574  rnghmsscmap  20575  funcrngcsetc  20585  rhmresfn  20593  dfringc2  20602  rhmsscmap2  20603  rhmsscmap  20604  rhmsscrnghm  20610  funcringcsetc  20619  rngcrescrhm  20629  rhmsubclem1  20630  rhmsubclem4  20633  lmhmlsp  20992  evpmss  21531  cssss  21630  frlmplusgval  21709  frlmvscafval  21711  uvcresum  21738  resspsrbas  21919  resspsrvsca  21922  subrgpsr  21923  mplsubglem  21944  ressmplbas  21971  subrgmpl  21975  opsrtoslem2  21999  mpfrcl  22028  ressply1bas  22149  ressply1evl  22293  evls1addd  22294  evls1muld  22295  evls1vsca  22296  evls1fvcl  22298  evls1maprhm  22299  scmatlss  22448  cpmatsubgpmat  22643  toponsspwpw  22845  basdif0  22876  ntrss2  22980  ordtbas2  23114  ordtbas  23115  cncls  23197  cmpfi  23331  comppfsc  23455  kgentopon  23461  ptpjpre1  23494  xkoccn  23542  prdstopn  23551  uzfbas  23821  utoptop  24158  utopbas  24159  setsmstopn  24402  restmetu  24494  tngtopn  24574  iccntr  24746  metdstri  24776  pi1xfrcnvlem  24992  cphsubrglem  25114  tcphcph  25174  rrxnm  25328  rrxbasefi  25347  ovolshftlem1  25447  ovolshft  25449  ovolscalem1  25451  ovolscalem2  25452  ovolsca  25453  uniioombllem2  25521  uniioombllem3a  25522  uniioombllem3  25523  uniioombllem4  25524  uniioombllem6  25526  itgioo  25754  limcnlp  25816  dvbsss  25840  dvcnvrelem1  25959  dvfsumle  25963  dvfsumleOLD  25964  dvfsumabs  25966  pserdv  26376  rlimcnp2  26912  fsumharmonic  26958  chpval2  27165  bday0b  27778  madef  27798  madess  27818  oldssmade  27819  n0sbday  28257  tglnssp  28463  perpln1  28621  perpln2  28622  uhgrspansubgr  29202  clwwlknclwwlkdifnum  29893  ocsh  31196  shsss  31226  speccl  31812  elnlfn  31841  pj3i  32121  sumdmdlem2  32332  fcoinver  32518  ffsrn  32641  ssnnssfz  32698  pfxrn2  32834  ccatws1f1o  32846  cycpmrn  33072  cycpmconjslem2  33084  inftmrel  33096  ressply1mon1p  33498  ressply1invg  33499  evls1subd  33502  algextdeglem7  33673  algextdeglem8  33674  smatrcl  33735  metidss  33830  fsumcvg4  33889  dya2iocuni  34223  carsgcl  34244  breprexplema  34583  bnj1143  34742  bnj1262  34762  bnj517  34837  kur14lem1  35149  cvmliftmolem2  35225  cvmliftlem15  35241  mrsubrn  35456  msubrn  35472  poimirlem30  37595  mblfinlem2  37603  sdclem2  37687  sstotbnd2  37719  isbnd3  37729  lkrlss  39034  pmapssat  39699  diass  40982  diaintclN  40998  dia2dimlem13  41016  dibintclN  41107  lcfrlem25  41507  lcdvbasess  41534  mapdin  41602  mplsubrgcl  42496  diophin  42720  rmxyelqirr  42858  itgocn  43113  oaabsb  43243  oege1  43255  oege2  43256  oacl2g  43279  tfsconcatb0  43293  ofoafg  43303  ofoaf  43304  fpwfvss  43361  relexp0a  43665  frege131d  43713  fsovrfovd  43958  clsk1indlem2  43991  clsk1indlem3  43992  mnuprd  44226  unirestss  45075  founiiun0  45141  fsumsupp0  45537  limsupequzlem  45681  dvnprodlem1  45905  ibliooicc  45930  stoweidlem34  45993  stoweidlem59  46018  etransclem24  46217  caratheodory  46487  ovnhoilem1  46560  hspdifhsp  46575  smfaddlem2  46723  smflimlem1  46730  smflimlem2  46731  smfmullem4  46753  smfsuplem1  46770  fcoreslem4  47023  fcoresf1  47026  fcoresfo  47028  dfnbgrss  47783  dfnbgrss2  47790  isubgrsubgr  47800  rngchomrnghmresALTV  48140  rngcrescrhmALTV  48141  rhmsubcALTVlem1  48142  funcringcsetcALTV2lem9  48159  ssnn0ssfz  48210  isclatd  48836  setrec2fun  49276  setrec2mpt  49281