Theorem eqsstrdi 3969

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-in 3888  df-ss 3898

This theorem is referenced by:  eqsstrrdi  3970  dmxpss  5995  dmsnopss  6038  iotassuni  6303  fvmptss  6757  fvmptss2  6770  fimacnv  6816  funressn  6898  riotassuni  7133  frxp  7803  suppssdm  7826  suppun  7833  suppss  7843  suppssov1  7845  suppss2  7847  suppssfv  7849  wfrlem15  7952  oawordeulem  8163  omwordri  8181  oewordri  8201  fodomr  8652  fipwuni  8874  fipwss  8877  ordtypelem6  8971  inf3lemd  9074  cantnfle  9118  cantnflem2  9137  en2other2  9420  ackbij1lem15  9645  ackbij2lem3  9652  cfub  9660  cflecard  9664  cfle  9665  fin23lem13  9743  fin23lem29  9752  compsscnvlem  9781  itunitc1  9831  fpwwe2lem12  10052  grur1a  10230  uzssz  12252  fsuppmapnn0fiublem  13353  fsuppmapnn0fiub  13354  swrdlend  14006  repswswrd  14137  cshimadifsn  14182  xptrrel  14331  relexpnndm  14392  relexpdmd  14395  relexprnd  14399  relexpfldd  14401  rtrclreclem4  14412  limsupgle  14826  isercolllem2  15014  isercolllem3  15015  isercoll  15016  fsumss  15074  sadcaddlem  15796  sadadd2lem  15798  sadadd3  15800  sadcl  15801  sadaddlem  15805  sadasslem  15809  sadeq  15811  smupvallem  15822  smucl  15823  prmreclem4  16245  prmreclem5  16246  1arith  16253  vdwmc2  16305  vdwlem13  16319  ramz2  16350  strfvss  16498  ressbasss  16548  prdsless  16728  sectss  17014  invss  17023  fullfunc  17168  fthfunc  17169  catccatid  17354  resscatc  17357  catcisolem  17358  catciso  17359  yoniso  17527  gsumpropd2lem  17881  cntzrcl  18449  cntzssv  18450  gsumzmhm  19050  ablfaclem3  19202  lmhmlsp  19814  evpmss  20275  cssss  20374  frlmplusgval  20453  frlmvscafval  20455  uvcresum  20482  resspsrbas  20653  resspsrvsca  20656  subrgpsr  20657  mplsubglem  20672  ressmplbas  20696  subrgmpl  20700  mpfrcl  20757  ressply1bas  20858  scmatlss  21130  cpmatsubgpmat  21325  toponsspwpw  21527  basdif0  21558  ntrss2  21662  ordtbas2  21796  ordtbas  21797  cncls  21879  cmpfi  22013  comppfsc  22137  kgentopon  22143  ptpjpre1  22176  xkoccn  22224  prdstopn  22233  uzfbas  22503  utoptop  22840  utopbas  22841  setsmstopn  23085  restmetu  23177  tngtopn  23256  iccntr  23426  metdstri  23456  pi1xfrcnvlem  23661  cphsubrglem  23782  tcphcph  23841  rrxnm  23995  rrxbasefi  24014  ovolshftlem1  24113  ovolshft  24115  ovolscalem1  24117  ovolscalem2  24118  ovolsca  24119  uniioombllem2  24187  uniioombllem3a  24188  uniioombllem3  24189  uniioombllem4  24190  uniioombllem6  24192  itgioo  24419  limcnlp  24481  dvbsss  24505  dvcnvrelem1  24620  dvfsumle  24624  dvfsumabs  24626  pserdv  25024  rlimcnp2  25552  fsumharmonic  25597  chpval2  25802  tglnssp  26346  perpln1  26504  perpln2  26505  uhgrspansubgr  27081  clwwlknclwwlkdifnum  27765  ocsh  29066  shsss  29096  speccl  29682  elnlfn  29711  pj3i  29991  sumdmdlem2  30202  fcoinver  30370  ffsrn  30491  ssnnssfz  30536  pfxrn2  30642  cycpmrn  30835  cycpmconjslem2  30847  inftmrel  30859  smatrcl  31149  metidss  31244  fsumcvg4  31303  dya2iocuni  31651  carsgcl  31672  breprexplema  32011  bnj1143  32172  bnj1262  32192  bnj517  32267  kur14lem1  32566  cvmliftmolem2  32642  cvmliftlem15  32658  mrsubrn  32873  msubrn  32889  trpredlem1  33179  poimirlem30  35087  mblfinlem2  35095  sdclem2  35180  sstotbnd2  35212  isbnd3  35222  lkrlss  36391  pmapssat  37055  diass  38338  diaintclN  38354  dia2dimlem13  38372  dibintclN  38463  lcfrlem25  38863  lcdvbasess  38890  mapdin  38958  diophin  39713  itgocn  40108  relexp0a  40417  frege131d  40465  fsovrfovd  40710  clsk1indlem2  40745  clsk1indlem3  40746  mnuprd  40984  unirestss  41759  founiiun0  41817  fsumsupp0  42220  limsupequzlem  42364  ibliooicc  42613  stoweidlem34  42676  stoweidlem59  42701  etransclem24  42900  caratheodory  43167  ovnhoilem1  43240  hspdifhsp  43255  smfaddlem2  43397  smflimlem1  43404  smflimlem2  43405  smfmullem4  43426  smfsuplem1  43442  rnghmresfn  44587  dfrngc2  44596  rnghmsscmap2  44597  rnghmsscmap  44598  rngchomrnghmresALTV  44620  funcrngcsetc  44622  rhmresfn  44633  dfringc2  44642  rhmsscmap2  44643  rhmsscmap  44644  rhmsscrnghm  44650  funcringcsetc  44659  funcringcsetcALTV2lem9  44668  rngcrescrhm  44709  rhmsubclem1  44710  rhmsubclem4  44713  rngcrescrhmALTV  44727  rhmsubcALTVlem1  44728  ssnn0ssfz  44751  setrec2fun  45222