Theorem eqsstrdi 3981

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

Syntax hints:   → wi 4   = wceq 1570   ⊆ wss 3905

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-cleq 2755  df-ss 3922

This theorem is referenced by:  eqsstrrdi  3982  eqimssd  3993  dmxpss  6169  dmsnopss  6215  iotassuni  6511  fvmptss  7002  fvmptss2  7016  funressn  7156  riotassuni  7407  ordsuci  7803  frxp  8118  suppssdm  8169  suppun  8176  suppss  8186  suppssov1  8189  suppssov2  8190  suppss2  8192  suppssfv  8194  oawordeulem  8535  omwordri  8553  oewordri  8574  mapssfset  8844  fodomr  9112  fodomfir  9283  fipwuni  9382  fipwss  9385  ordtypelem6  9481  inf3lemd  9592  cantnfle  9636  cantnflem2  9655  ttrclselem1  9690  en2other2  9989  ackbij1lem15  10212  ackbij2lem3  10219  cfub  10227  cflecard  10231  cfle  10232  fin23lem13  10311  fin23lem29  10320  compsscnvlem  10349  itunitc1  10399  fpwwe2lem11  10621  grur1a  10799  uzssz  12878  fsuppmapnn0fiublem  14022  fsuppmapnn0fiub  14023  swrdlend  14687  repswswrd  14817  cshimadifsn  14862  xptrrel  15013  relexpnndm  15074  relexpdmd  15077  relexprnd  15081  relexpfldd  15083  rtrclreclem4  15094  limsupgle  15524  isercolllem2  15713  isercolllem3  15714  isercoll  15715  fsumss  15772  sadcaddlem  16510  sadadd2lem  16512  sadadd3  16514  sadcl  16515  sadaddlem  16519  sadasslem  16523  sadeq  16525  smupvallem  16536  smucl  16537  prmreclem4  16974  prmreclem5  16975  1arith  16982  vdwmc2  17034  vdwlem13  17048  ramz2  17079  strfvss  17242  ressbasssg  17292  ressbasssOLD  17295  prdsless  17511  sectss  17804  invss  17813  fullfunc  17960  fthfunc  17961  catccatid  18158  resscatc  18161  catcisolem  18162  catciso  18163  yoniso  18336  gsumpropd2lem  18732  cntzrcl  19392  cntzssv  19393  gsumzmhm  20002  ablfaclem3  20154  rnghmresfn  20718  dfrngc2  20727  rnghmsscmap2  20728  rnghmsscmap  20729  funcrngcsetc  20739  rhmresfn  20747  dfringc2  20756  rhmsscmap2  20757  rhmsscmap  20758  rhmsscrnghm  20764  funcringcsetc  20773  rngcrescrhm  20783  rhmsubclem1  20784  rhmsubclem4  20787  lmhmlsp  21170  evpmss  21736  cssss  21835  frlmplusgval  21914  frlmvscafval  21916  uvcresum  21943  resspsrbas  22123  resspsrvsca  22126  subrgpsr  22127  mplsubglem  22148  ressmplbas  22178  subrgmpl  22182  mplsubrgcl  22183  opsrtoslem2  22207  mpfrcl  22236  ressply1bas  22388  ressply1evl  22530  evls1addd  22531  evls1muld  22532  evls1vsca  22533  evls1fvcl  22535  evls1maprhm  22536  scmatlss  22682  cpmatsubgpmat  22877  toponsspwpw  23079  basdif0  23110  ntrss2  23214  ordtbas2  23348  ordtbas  23349  cncls  23431  cmpfi  23565  comppfsc  23689  kgentopon  23695  ptpjpre1  23728  xkoccn  23776  prdstopn  23785  uzfbas  24055  utoptop  24391  utopbas  24392  setsmstopn  24635  restmetu  24727  tngtopn  24807  iccntr  24979  metdstri  25009  pi1xfrcnvlem  25215  cphsubrglem  25336  tcphcph  25396  rrxnm  25550  rrxbasefi  25569  ovolshftlem1  25668  ovolshft  25670  ovolscalem1  25672  ovolscalem2  25673  ovolsca  25674  uniioombllem2  25742  uniioombllem3a  25743  uniioombllem3  25744  uniioombllem4  25745  uniioombllem6  25747  itgioo  25975  limcnlp  26037  dvbsss  26061  dvcnvrelem1  26176  dvfsumle  26180  dvfsumabs  26182  pserdv  26592  rlimcnp2  27131  fsumharmonic  27176  chpval2  27382  bday0b  28006  madef  28029  madess  28059  oldssmade  28060  oldss  28063  n0bday  28545  bdayn0p1  28562  bdaypw2n0bndlem  28656  bdaypw2n0bnd  28657  tglnssp  28821  perpln1  28990  perpln2  28991  uhgrspansubgr  29641  clwwlknclwwlkdifnum  30331  ocsh  31635  shsss  31665  speccl  32251  elnlfn  32280  pj3i  32560  sumdmdlem2  32771  fcoinver  32949  ffsrn  33073  ssnnssfz  33132  pfxrn2  33260  ccatws1f1o  33271  cycpmrn  33463  cycpmconjslem2  33475  fxpss  33486  inftmrel  33500  ressply1mon1p  33858  ressply1invg  33859  evls1subd  33862  esplyind  33965  algextdeglem7  34113  algextdeglem8  34114  smatrcl  34186  metidss  34281  fsumcvg4  34340  dya2iocuni  34673  carsgcl  34694  breprexplema  35017  bnj1143  35178  bnj1262  35198  bnj517  35273  kur14lem1  35698  cvmliftmolem2  35774  cvmliftlem15  35790  mrsubrn  36005  msubrn  36021  dfttc2g  37017  poimirlem30  38301  mblfinlem2  38309  sdclem2  38393  sstotbnd2  38425  isbnd3  38435  lkrlss  39869  pmapssat  40533  diass  41816  diaintclN  41832  dia2dimlem13  41850  dibintclN  41941  lcfrlem25  42341  lcdvbasess  42368  mapdin  42436  diophin  43503  rmxyelqirr  43637  itgocn  43891  oaabsb  44021  oege1  44033  oege2  44034  oacl2g  44057  tfsconcatb0  44071  ofoafg  44081  ofoaf  44082  fpwfvss  44138  relexp0a  44442  frege131d  44490  fsovrfovd  44735  clsk1indlem2  44768  clsk1indlem3  44769  mnuprd  44986  unirestss  45842  founiiun0  45908  fsumsupp0  46294  limsupequzlem  46436  dvnprodlem1  46660  ibliooicc  46685  stoweidlem34  46748  stoweidlem59  46773  etransclem24  46972  caratheodory  47242  ovnhoilem1  47315  hspdifhsp  47330  sssmf  47452  smfaddlem2  47478  smflimlem1  47485  smflimlem2  47486  smfmullem4  47508  smfsuplem1  47525  fcoreslem4  47803  fcoresf1  47806  fcoresfo  47808  dfnbgrss  48617  dfnbgrss2  48624  isubgrsubgr  48634  rngchomrnghmresALTV  49044  rngcrescrhmALTV  49045  rhmsubcALTVlem1  49046  funcringcsetcALTV2lem9  49063  ssnn0ssfz  49129  isclatd  49761  nelsubclem  49845  setrec2fun  50470  setrec2mpt  50475