Theorem eqsstrdi 4008

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

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

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 2008  ax-9 2119  ax-ext 2708

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

This theorem is referenced by:  eqsstrrdi  4009  eqimssd  4020  dmxpss  6165  dmsnopss  6208  iotassuni  6508  iotassuniOLD  6515  fvmptss  7003  fvmptss2  7017  funressn  7154  riotassuni  7407  ordsuci  7807  frxp  8130  suppssdm  8181  suppun  8188  suppss  8198  suppssov1  8201  suppssov2  8202  suppss2  8204  suppssfv  8206  wfrlem15OLD  8342  oawordeulem  8571  omwordri  8589  oewordri  8609  mapssfset  8870  fodomr  9147  fodomfir  9345  fipwuni  9443  fipwss  9446  ordtypelem6  9542  inf3lemd  9646  cantnfle  9690  cantnflem2  9709  ttrclselem1  9744  en2other2  10028  ackbij1lem15  10252  ackbij2lem3  10259  cfub  10268  cflecard  10272  cfle  10273  fin23lem13  10351  fin23lem29  10360  compsscnvlem  10389  itunitc1  10439  fpwwe2lem11  10660  grur1a  10838  uzssz  12878  fsuppmapnn0fiublem  14013  fsuppmapnn0fiub  14014  swrdlend  14676  repswswrd  14807  cshimadifsn  14853  xptrrel  15004  relexpnndm  15065  relexpdmd  15068  relexprnd  15072  relexpfldd  15074  rtrclreclem4  15085  limsupgle  15498  isercolllem2  15687  isercolllem3  15688  isercoll  15689  fsumss  15746  sadcaddlem  16481  sadadd2lem  16483  sadadd3  16485  sadcl  16486  sadaddlem  16490  sadasslem  16494  sadeq  16496  smupvallem  16507  smucl  16508  prmreclem4  16944  prmreclem5  16945  1arith  16952  vdwmc2  17004  vdwlem13  17018  ramz2  17049  strfvss  17211  ressbasssg  17263  ressbasssOLD  17266  prdsless  17482  sectss  17770  invss  17779  fullfunc  17926  fthfunc  17927  catccatid  18124  resscatc  18127  catcisolem  18128  catciso  18129  yoniso  18302  gsumpropd2lem  18662  cntzrcl  19315  cntzssv  19316  gsumzmhm  19923  ablfaclem3  20075  rnghmresfn  20584  dfrngc2  20593  rnghmsscmap2  20594  rnghmsscmap  20595  funcrngcsetc  20605  rhmresfn  20613  dfringc2  20622  rhmsscmap2  20623  rhmsscmap  20624  rhmsscrnghm  20630  funcringcsetc  20639  rngcrescrhm  20649  rhmsubclem1  20650  rhmsubclem4  20653  lmhmlsp  21012  evpmss  21551  cssss  21650  frlmplusgval  21729  frlmvscafval  21731  uvcresum  21758  resspsrbas  21939  resspsrvsca  21942  subrgpsr  21943  mplsubglem  21964  ressmplbas  21991  subrgmpl  21995  opsrtoslem2  22019  mpfrcl  22048  ressply1bas  22169  ressply1evl  22313  evls1addd  22314  evls1muld  22315  evls1vsca  22316  evls1fvcl  22318  evls1maprhm  22319  scmatlss  22468  cpmatsubgpmat  22663  toponsspwpw  22865  basdif0  22896  ntrss2  23000  ordtbas2  23134  ordtbas  23135  cncls  23217  cmpfi  23351  comppfsc  23475  kgentopon  23481  ptpjpre1  23514  xkoccn  23562  prdstopn  23571  uzfbas  23841  utoptop  24178  utopbas  24179  setsmstopn  24422  restmetu  24514  tngtopn  24594  iccntr  24766  metdstri  24796  pi1xfrcnvlem  25012  cphsubrglem  25134  tcphcph  25194  rrxnm  25348  rrxbasefi  25367  ovolshftlem1  25467  ovolshft  25469  ovolscalem1  25471  ovolscalem2  25472  ovolsca  25473  uniioombllem2  25541  uniioombllem3a  25542  uniioombllem3  25543  uniioombllem4  25544  uniioombllem6  25546  itgioo  25774  limcnlp  25836  dvbsss  25860  dvcnvrelem1  25979  dvfsumle  25983  dvfsumleOLD  25984  dvfsumabs  25986  pserdv  26396  rlimcnp2  26933  fsumharmonic  26979  chpval2  27186  bday0b  27799  madef  27821  madess  27845  oldssmade  27846  n0sbday  28301  bdayn0p1  28315  tglnssp  28536  perpln1  28694  perpln2  28695  uhgrspansubgr  29275  clwwlknclwwlkdifnum  29966  ocsh  31269  shsss  31299  speccl  31885  elnlfn  31914  pj3i  32194  sumdmdlem2  32405  fcoinver  32590  ffsrn  32711  ssnnssfz  32769  pfxrn2  32920  ccatws1f1o  32932  cycpmrn  33159  cycpmconjslem2  33171  inftmrel  33183  ressply1mon1p  33586  ressply1invg  33587  evls1subd  33590  algextdeglem7  33762  algextdeglem8  33763  smatrcl  33832  metidss  33927  fsumcvg4  33986  dya2iocuni  34320  carsgcl  34341  breprexplema  34667  bnj1143  34826  bnj1262  34846  bnj517  34921  kur14lem1  35233  cvmliftmolem2  35309  cvmliftlem15  35325  mrsubrn  35540  msubrn  35556  poimirlem30  37679  mblfinlem2  37687  sdclem2  37771  sstotbnd2  37803  isbnd3  37813  lkrlss  39118  pmapssat  39783  diass  41066  diaintclN  41082  dia2dimlem13  41100  dibintclN  41191  lcfrlem25  41591  lcdvbasess  41618  mapdin  41686  mplsubrgcl  42546  diophin  42770  rmxyelqirr  42908  itgocn  43163  oaabsb  43293  oege1  43305  oege2  43306  oacl2g  43329  tfsconcatb0  43343  ofoafg  43353  ofoaf  43354  fpwfvss  43411  relexp0a  43715  frege131d  43763  fsovrfovd  44008  clsk1indlem2  44041  clsk1indlem3  44042  mnuprd  44275  unirestss  45128  founiiun0  45194  fsumsupp0  45587  limsupequzlem  45731  dvnprodlem1  45955  ibliooicc  45980  stoweidlem34  46043  stoweidlem59  46068  etransclem24  46267  caratheodory  46537  ovnhoilem1  46610  hspdifhsp  46625  smfaddlem2  46773  smflimlem1  46780  smflimlem2  46781  smfmullem4  46803  smfsuplem1  46820  fcoreslem4  47075  fcoresf1  47078  fcoresfo  47080  dfnbgrss  47845  dfnbgrss2  47852  isubgrsubgr  47862  rngchomrnghmresALTV  48234  rngcrescrhmALTV  48235  rhmsubcALTVlem1  48236  funcringcsetcALTV2lem9  48253  ssnn0ssfz  48304  isclatd  48937  nelsubclem  49014  setrec2fun  49536  setrec2mpt  49541