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 1539   ⊆ wss 3886

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-v 3431  df-in 3893  df-ss 3903

This theorem is referenced by:  eqsstrrdi  3975  dmxpss  6067  dmsnopss  6110  iotassuni  6405  fvmptss  6879  fvmptss2  6892  fimacnvOLD  6940  funressn  7023  riotassuni  7265  frxp  7954  suppssdm  7980  suppun  7987  suppss  7997  suppssOLD  7998  suppssov1  8001  suppss2  8003  suppssfv  8005  wfrlem15OLD  8141  oawordeulem  8372  omwordri  8390  oewordri  8410  mapssfset  8626  fodomr  8902  fipwuni  9172  fipwss  9175  ordtypelem6  9269  inf3lemd  9372  cantnfle  9416  cantnflem2  9435  ttrclselem1  9470  trpredlem1  9483  en2other2  9775  ackbij1lem15  10000  ackbij2lem3  10007  cfub  10015  cflecard  10019  cfle  10020  fin23lem13  10098  fin23lem29  10107  compsscnvlem  10136  itunitc1  10186  fpwwe2lem11  10407  grur1a  10585  uzssz  12613  fsuppmapnn0fiublem  13720  fsuppmapnn0fiub  13721  swrdlend  14376  repswswrd  14507  cshimadifsn  14552  xptrrel  14701  relexpnndm  14762  relexpdmd  14765  relexprnd  14769  relexpfldd  14771  rtrclreclem4  14782  limsupgle  15196  isercolllem2  15387  isercolllem3  15388  isercoll  15389  fsumss  15447  sadcaddlem  16174  sadadd2lem  16176  sadadd3  16178  sadcl  16179  sadaddlem  16183  sadasslem  16187  sadeq  16189  smupvallem  16200  smucl  16201  prmreclem4  16630  prmreclem5  16631  1arith  16638  vdwmc2  16690  vdwlem13  16704  ramz2  16735  strfvss  16898  ressbasss  16960  prdsless  17184  sectss  17474  invss  17483  fullfunc  17632  fthfunc  17633  catccatid  17831  resscatc  17834  catcisolem  17835  catciso  17836  yoniso  18013  gsumpropd2lem  18373  cntzrcl  18943  cntzssv  18944  gsumzmhm  19548  ablfaclem3  19700  lmhmlsp  20321  evpmss  20801  cssss  20900  frlmplusgval  20981  frlmvscafval  20983  uvcresum  21010  resspsrbas  21194  resspsrvsca  21197  subrgpsr  21198  mplsubglem  21215  ressmplbas  21239  subrgmpl  21243  mpfrcl  21305  ressply1bas  21410  scmatlss  21684  cpmatsubgpmat  21879  toponsspwpw  22081  basdif0  22113  ntrss2  22218  ordtbas2  22352  ordtbas  22353  cncls  22435  cmpfi  22569  comppfsc  22693  kgentopon  22699  ptpjpre1  22732  xkoccn  22780  prdstopn  22789  uzfbas  23059  utoptop  23396  utopbas  23397  setsmstopn  23643  restmetu  23736  tngtopn  23824  iccntr  23994  metdstri  24024  pi1xfrcnvlem  24229  cphsubrglem  24351  tcphcph  24411  rrxnm  24565  rrxbasefi  24584  ovolshftlem1  24683  ovolshft  24685  ovolscalem1  24687  ovolscalem2  24688  ovolsca  24689  uniioombllem2  24757  uniioombllem3a  24758  uniioombllem3  24759  uniioombllem4  24760  uniioombllem6  24762  itgioo  24990  limcnlp  25052  dvbsss  25076  dvcnvrelem1  25191  dvfsumle  25195  dvfsumabs  25197  pserdv  25598  rlimcnp2  26126  fsumharmonic  26171  chpval2  26376  tglnssp  26923  perpln1  27081  perpln2  27082  uhgrspansubgr  27668  clwwlknclwwlkdifnum  28352  ocsh  29653  shsss  29683  speccl  30269  elnlfn  30298  pj3i  30578  sumdmdlem2  30789  fcoinver  30954  ffsrn  31072  ssnnssfz  31116  pfxrn2  31222  cycpmrn  31418  cycpmconjslem2  31430  inftmrel  31442  smatrcl  31754  metidss  31849  fsumcvg4  31908  dya2iocuni  32258  carsgcl  32279  breprexplema  32618  bnj1143  32778  bnj1262  32798  bnj517  32873  kur14lem1  33176  cvmliftmolem2  33252  cvmliftlem15  33268  mrsubrn  33483  msubrn  33499  bday0b  34032  madef  34048  madess  34067  oldssmade  34068  poimirlem30  35815  mblfinlem2  35823  sdclem2  35908  sstotbnd2  35940  isbnd3  35950  lkrlss  37117  pmapssat  37781  diass  39064  diaintclN  39080  dia2dimlem13  39098  dibintclN  39189  lcfrlem25  39589  lcdvbasess  39616  mapdin  39684  eqimssd  40191  sn-iotassuni  40204  diophin  40602  itgocn  40997  relexp0a  41305  frege131d  41353  fsovrfovd  41598  clsk1indlem2  41633  clsk1indlem3  41634  mnuprd  41875  unirestss  42654  founiiun0  42709  fsumsupp0  43100  limsupequzlem  43244  ibliooicc  43493  stoweidlem34  43556  stoweidlem59  43581  etransclem24  43780  caratheodory  44047  ovnhoilem1  44120  hspdifhsp  44135  smfaddlem2  44277  smflimlem1  44284  smflimlem2  44285  smfmullem4  44306  smfsuplem1  44322  fcoreslem4  44538  fcoresf1  44541  fcoresfo  44543  rnghmresfn  45499  dfrngc2  45508  rnghmsscmap2  45509  rnghmsscmap  45510  rngchomrnghmresALTV  45532  funcrngcsetc  45534  rhmresfn  45545  dfringc2  45554  rhmsscmap2  45555  rhmsscmap  45556  rhmsscrnghm  45562  funcringcsetc  45571  funcringcsetcALTV2lem9  45580  rngcrescrhm  45621  rhmsubclem1  45622  rhmsubclem4  45625  rngcrescrhmALTV  45639  rhmsubcALTVlem1  45640  ssnn0ssfz  45663  isclatd  46247  setrec2fun  46376