Theorem eqsstrdi 3974

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

Syntax hints:   → wi 4   = wceq 1538   ⊆ wss 3886

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 1910  ax-6 1968  ax-7 2008  ax-8 2105  ax-9 2113  ax-ext 2706

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1541  df-ex 1779  df-sb 2065  df-clab 2713  df-cleq 2727  df-clel 2813  df-v 3433  df-in 3893  df-ss 3903

This theorem is referenced by:  eqsstrrdi  3975  dmxpss  6077  dmsnopss  6120  iotassuni  6414  fvmptss  6894  fvmptss2  6907  fimacnvOLD  6955  funressn  7038  riotassuni  7280  frxp  7974  suppssdm  8000  suppun  8007  suppss  8017  suppssOLD  8018  suppssov1  8021  suppss2  8023  suppssfv  8025  wfrlem15OLD  8161  oawordeulem  8392  omwordri  8410  oewordri  8430  mapssfset  8646  fodomr  8922  fipwuni  9192  fipwss  9195  ordtypelem6  9289  inf3lemd  9392  cantnfle  9436  cantnflem2  9455  ttrclselem1  9490  en2other2  9772  ackbij1lem15  9997  ackbij2lem3  10004  cfub  10012  cflecard  10016  cfle  10017  fin23lem13  10095  fin23lem29  10104  compsscnvlem  10133  itunitc1  10183  fpwwe2lem11  10404  grur1a  10582  uzssz  12610  fsuppmapnn0fiublem  13717  fsuppmapnn0fiub  13718  swrdlend  14373  repswswrd  14504  cshimadifsn  14549  xptrrel  14698  relexpnndm  14759  relexpdmd  14762  relexprnd  14766  relexpfldd  14768  rtrclreclem4  14779  limsupgle  15193  isercolllem2  15384  isercolllem3  15385  isercoll  15386  fsumss  15444  sadcaddlem  16171  sadadd2lem  16173  sadadd3  16175  sadcl  16176  sadaddlem  16180  sadasslem  16184  sadeq  16186  smupvallem  16197  smucl  16198  prmreclem4  16627  prmreclem5  16628  1arith  16635  vdwmc2  16687  vdwlem13  16701  ramz2  16732  strfvss  16895  ressbasss  16957  prdsless  17181  sectss  17471  invss  17480  fullfunc  17629  fthfunc  17630  catccatid  17828  resscatc  17831  catcisolem  17832  catciso  17833  yoniso  18010  gsumpropd2lem  18370  cntzrcl  18940  cntzssv  18941  gsumzmhm  19545  ablfaclem3  19697  lmhmlsp  20318  evpmss  20798  cssss  20897  frlmplusgval  20978  frlmvscafval  20980  uvcresum  21007  resspsrbas  21191  resspsrvsca  21194  subrgpsr  21195  mplsubglem  21212  ressmplbas  21236  subrgmpl  21240  mpfrcl  21302  ressply1bas  21407  scmatlss  21681  cpmatsubgpmat  21876  toponsspwpw  22078  basdif0  22110  ntrss2  22215  ordtbas2  22349  ordtbas  22350  cncls  22432  cmpfi  22566  comppfsc  22690  kgentopon  22696  ptpjpre1  22729  xkoccn  22777  prdstopn  22786  uzfbas  23056  utoptop  23393  utopbas  23394  setsmstopn  23640  restmetu  23733  tngtopn  23821  iccntr  23991  metdstri  24021  pi1xfrcnvlem  24226  cphsubrglem  24348  tcphcph  24408  rrxnm  24562  rrxbasefi  24581  ovolshftlem1  24680  ovolshft  24682  ovolscalem1  24684  ovolscalem2  24685  ovolsca  24686  uniioombllem2  24754  uniioombllem3a  24755  uniioombllem3  24756  uniioombllem4  24757  uniioombllem6  24759  itgioo  24987  limcnlp  25049  dvbsss  25073  dvcnvrelem1  25188  dvfsumle  25192  dvfsumabs  25194  pserdv  25595  rlimcnp2  26123  fsumharmonic  26168  chpval2  26373  tglnssp  26920  perpln1  27078  perpln2  27079  uhgrspansubgr  27665  clwwlknclwwlkdifnum  28351  ocsh  29652  shsss  29682  speccl  30268  elnlfn  30297  pj3i  30577  sumdmdlem2  30788  fcoinver  30953  ffsrn  31071  ssnnssfz  31115  pfxrn2  31221  cycpmrn  31417  cycpmconjslem2  31429  inftmrel  31441  smatrcl  31753  metidss  31848  fsumcvg4  31907  dya2iocuni  32257  carsgcl  32278  breprexplema  32617  bnj1143  32777  bnj1262  32797  bnj517  32872  kur14lem1  33175  cvmliftmolem2  33251  cvmliftlem15  33267  mrsubrn  33482  msubrn  33498  bday0b  34031  madef  34047  madess  34066  oldssmade  34067  poimirlem30  35814  mblfinlem2  35822  sdclem2  35907  sstotbnd2  35939  isbnd3  35949  lkrlss  37114  pmapssat  37778  diass  39061  diaintclN  39077  dia2dimlem13  39095  dibintclN  39186  lcfrlem25  39586  lcdvbasess  39613  mapdin  39681  eqimssd  40188  sn-iotassuni  40201  diophin  40599  itgocn  40994  relexp0a  41329  frege131d  41377  fsovrfovd  41622  clsk1indlem2  41657  clsk1indlem3  41658  mnuprd  41899  unirestss  42678  founiiun0  42739  fsumsupp0  43135  limsupequzlem  43279  ibliooicc  43528  stoweidlem34  43591  stoweidlem59  43616  etransclem24  43815  caratheodory  44083  ovnhoilem1  44156  hspdifhsp  44171  smfaddlem2  44319  smflimlem1  44326  smflimlem2  44327  smfmullem4  44349  smfsuplem1  44365  fcoreslem4  44581  fcoresf1  44584  fcoresfo  44586  rnghmresfn  45542  dfrngc2  45551  rnghmsscmap2  45552  rnghmsscmap  45553  rngchomrnghmresALTV  45575  funcrngcsetc  45577  rhmresfn  45588  dfringc2  45597  rhmsscmap2  45598  rhmsscmap  45599  rhmsscrnghm  45605  funcringcsetc  45614  funcringcsetcALTV2lem9  45623  rngcrescrhm  45664  rhmsubclem1  45665  rhmsubclem4  45668  rngcrescrhmALTV  45682  rhmsubcALTVlem1  45683  ssnn0ssfz  45706  isclatd  46290  setrec2fun  46419