Theorem eqsstri 3977

Description: Substitution of equality into a subclass relationship. (Contributed by NM, 16-Jul-1995.)

Hypotheses

Ref	Expression
eqsstr.1	⊢ 𝐴 = 𝐵
eqsstr.2	⊢ 𝐵 ⊆ 𝐶

Assertion

Ref	Expression
eqsstri	⊢ 𝐴 ⊆ 𝐶

Proof of Theorem eqsstri

Step	Hyp	Ref	Expression
1		eqsstr.2	. 2 ⊢ 𝐵 ⊆ 𝐶
2		eqsstr.1	. . 3 ⊢ 𝐴 = 𝐵
3	2	sseq1i 3959	. 2 ⊢ (𝐴 ⊆ 𝐶 ↔ 𝐵 ⊆ 𝐶)
4	1, 3	mpbir 234	1 ⊢ 𝐴 ⊆ 𝐶

This proof depends on syntax axioms:   = wceq 1570   ⊆ wss 3899

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2752  df-ss 3916

This theorem is used by:  eqsstrri  3978  3sstr4i  3982  ssrab3  4030  rabssab  4033  ifssun  4500  opabss  5169  brab2a  5748  relopabiALT  5804  dmopabss  5902  rnopabss  5939  resss  5994  relres  5998  rninOLD  6138  rnxpss  6165  cnvcnvss  6187  cnvcnvssOLD  6188  resdmss  6231  resssxp  6267  dfpo2  6294  predss  6307  fnres  6660  f0  6757  nfvres  6917  fvopab4ndm  7018  ffvresb  7120  mptexgf  7222  funiunfv  7246  isoini2  7341  ovssunirn  7450  dmoprabss  7518  mpondm0  7655  elmpocl  7656  exse2  7915  frxp  8125  tposssxp  8229  dftpos4  8244  smores  8342  smores2  8344  iordsmo  8347  swoer  8731  swoord1  8732  swoord2  8733  ecss  8751  ecopovsym  8822  ecopovtrn  8823  ecopover  8824  f1setex  8861  sbthlem7  9094  imafi  9288  elfiun  9403  marypha1lem  9406  marypha2lem1  9408  hartogslem1  9517  wdomima2g  9561  inf3lem1  9610  dmttrcl  9703  rnttrcl  9704  tc2  9722  frmin  9734  frrlem16  9743  frr1  9744  tz9.12lem1  9772  rankuni  9848  rankuniss  9851  rankmapu  9863  hta  9904  htaOLD  9905  r0weon  10018  infxpenlem  10019  ackbij1lem9  10232  ackbij1lem10  10233  ackbij1b  10243  sdom2en01  10307  fin23lem26  10330  fin56  10398  fin1a2lem9  10413  axdc3lem  10455  axdc3lem2  10456  axcclem  10462  imadomg  10540  iundom2g  10551  smobeth  10598  canth4  10659  gruina  10830  grur1a  10831  pinn  10890  niex  10893  ltsopi  10900  ltrelpi  10901  dmaddpi  10902  dmmulpi  10903  enqex  10934  ltrelnq  10938  nqerf  10942  nqerrel  10944  dmrecnq  10980  lterpq  10982  ltrelpr  11010  enrex  11079  ltrelsr  11080  dmaddsr  11097  dmmulsr  11098  ltrelre  11146  axaddf  11157  axmulf  11158  ltrelxr  11297  lerelxr  11299  nn0ssre  12535  nn0sscn  12536  nn0ssz  12641  uzsupss  12992  rpnnen1lem1  13031  rpnnen1lem3  13032  rpnnen1lem5  13034  fz1ssfz0  13681  uzsup  13927  fzfi  14039  swrd00  14715  01sqrexlem3  15334  cau3  15446  caubnd  15449  limsupgre  15571  rlimpm  15590  rlimclim  15636  isercolllem1  15755  isercolllem2  15756  isercoll  15758  caurcvg  15767  caucvg  15769  iseraltlem2  15773  iseraltlem3  15774  zsum  15807  fsumcvg3  15818  climfsum  15910  ackbijnn  15920  divcnvshft  15947  infcvgaux1i  15949  clim2prod  15980  ntrivcvg  15989  ntrivcvgfvn0  15991  ntrivcvgtail  15992  ntrivcvgmullem  15993  ntrivcvgmul  15994  zprod  16027  dvdszrcl  16350  4sqlem1  17043  4sqlem19  17058  ramub1lem2  17122  structcnvcnv  17248  strleun  17252  fvsetsid  17263  idressidex0  18776  smndex1sgrp  19023  gicer  19407  cntzsgrpcl  19464  symgbasfi  19509  mvdco  19575  symgsssg  19597  efglem  19846  efgtf  19852  efgtlen  19856  efginvrel2  19857  efginvrel1  19858  efgsfo  19869  efgredlemg  19872  efgredleme  19873  efgredlemd  19874  efgredlemc  19875  efgredlem  19877  efgred  19878  efgrelexlemb  19880  efgcpbllemb  19885  frgpinv  19894  frgpuplem  19902  frgpupf  19903  frgpup1  19905  frgpnabllem2  20004  gsumval3lem1  20035  gsumval3lem2  20036  gsumval3  20037  ricrel  20658  fldc  20953  fldhmsubc  20954  lbsextlem3  21350  pzriprnglem10  21706  znf1o  21767  zntoslem  21772  pjpm  21924  mhp0cl  22377  ply1bascl  22431  dmtopon  23151  ordtbas  23420  leordtval2  23440  lecldbas  23447  lmfval  23460  lmbrf  23488  cnconst2  23511  conncompcld  23662  hauspwdom  23730  txuni2  23794  xkouni  23828  xkoccn  23848  txkgen  23881  qtoptop2  23928  kqdisj  23961  hmphtop  24007  hmpher  24013  uzrest  24126  uzfbas  24127  lmflf  24234  tgpconncompeqg  24341  tgpconncomp  24342  ustn0  24450  xmeter  24662  isngp2  24826  xrtgioo  25036  iccntr  25051  xmetdcn  25068  metdcn  25070  metdscn2  25087  cnheiborlem  25185  reparphti  25228  lmmbrf  25493  iscau4  25510  iscauf  25511  caucfil  25514  lmclimf  25535  volf  25760  uniioombllem3  25816  uniioombllem4  25817  uniioombllem5  25818  volcn  25837  mbfimaopnlem  25886  mbflimsup  25897  i1f1  25921  itg2lcl  25958  itgioo  26046  itgsplitioo  26068  limcflflem  26110  limcflf  26111  limcresi  26115  lhop  26246  dvfsumlem1  26256  dvfsumlem2  26257  dvfsumlem3  26258  dvfsumlem4  26259  dvfsumrlimge0  26260  dvfsumrlim  26261  dvfsumrlim2  26262  dvfsum2  26264  vieta1lem1  26545  vieta1lem2  26546  psercnlem2  26663  psercnlem1  26664  psercn  26665  pserdvlem1  26666  pserdvlem2  26667  pserdv  26668  pserdv2  26669  logcnlem5  26886  dvlog  26891  dvlog2lem  26892  dvlog2  26893  dvcncxp1  26983  dvcnsqrt  26984  cxpcn3lem  26987  cxpcn3  26988  sqrtcn  26990  1cubr  27082  atansssdm  27173  jensen  27228  musum  27430  ppiub  27443  lgsquadlem1  27619  lgsquadlem2  27620  lgsquadlem3  27621  2sqlem7  27663  nosupbnd1lem1  27947  nosupbnd2  27955  noinfbnd1lem1  27962  cutsf  28060  leftssold  28139  rightssold  28140  mulsproplem12  28395  mulsproplem13  28396  mulsproplem14  28397  precsexlem8  28482  onssno  28522  nnssn0s  28589  dfnns2  28640  bdaypw2n0bndlem  28731  axtgcgrrflx  28806  axtgcgrid  28807  axtgsegcon  28808  axtg5seg  28809  axtgbtwnid  28810  axtgpasch  28811  axtgcont1  28812  tglng  28891  disjxwwlkn  30384  frgrwopreg2  30802  phnv  31298  htthlem  31401  hlimadd  31677  hlimcaui  31720  hhsscms  31762  occllem  31787  shjshsi  31976  3oalem4  32149  pjfi  32188  dmadjss  32371  nlelshi  32544  nlelchi  32545  hmopidmchi  32635  shatomistici  32845  difxp1ss  33000  difxp2ss  33001  fcoinver  33080  opabssi  33089  mptctf  33190  ccatws1f1o  33396  gsumpart  33506  pmtrcnel2  33533  psgnfzto1stlem  33543  cycpmrn  33586  cyc3genpm  33595  unitprodclb  33825  lsmsnorb  33827  ply1degltel  34007  ply1degleel  34008  ply1degltlss  34009  evlextv  34055  vietalem  34092  constrsscn  34253  cnre2csqima  34424  raddcn  34442  zrhcntr  34492  rrhre  34534  esumsnf  34577  sxbrsiga  34804  omssubadd  34814  carsggect  34832  sitmcl  34865  oddpwdc  34868  eulerpartlem1  34881  eulerpartlemt  34885  eulerpartgbij  34886  eulerpartlemmf  34889  eulerpartlemgh  34892  sseqf  34906  ballotlemfmpn  35009  ballotth  35052  signswch  35072  ftc2re  35109  fdvposlt  35110  fdvposle  35112  bnj1146  35303  bnj1292  35327  bnj1293  35328  bnj1145  35505  bnj1177  35518  fineqvnttrclse  35653  tz9.1regs  35663  erdszelem2  35774  kur14lem3  35790  kur14lem6  35793  kur14lem7  35794  kur14lem9  35796  cvmlift2lem12  35896  mpstssv  36121  mstapst  36129  mppspstlem  36153  mppspst  36156  mthmsta  36160  mthmpps  36164  mclsppslem  36165  txpss3v  36458  pprodss4v  36464  relsset  36468  fixssdm  36486  fixssrn  36487  limitssson  36491  funpartss  36526  colinearex  36643  fneer  36975  neibastop1  36981  neibastop2lem  36982  filnetlem2  37001  filnetlem3  37002  ttcuniun  37132  ttcuni  37135  knoppcnlem10  37202  bj-tagss  37727  bj-imdirco  37945  bj-fvsnun2  38011  bj-ablssgrp  38031  bj-ablsscmn  38033  bj-vecssmod  38036  bj-fldssdrng  38043  icoreresf  38109  icoreunrn  38116  poimirlem29  38401  poimirlem30  38402  poimirlem31  38403  poimir  38405  broucube  38406  dvasin  38456  dvacos  38457  areacirc  38465  caures  38513  bnd2lem  38544  ismtyres  38561  flddivrng  38752  xrnss3v  39132  refrelsredund2  39468  toycom  39849  dihglblem2N  42170  lcdvbase  42469  mapdunirnN  42526  aks6d1c1p1rcl  42977  redvmptabs  43238  readvrec  43240  prjspreln0  43458  prjspvs  43459  prjspeclsp  43461  0prjspnrel  43476  dffltz  43483  eldiophb  43605  monotuz  43785  pwssplit4  43933  pwfi2f1o  43940  arearect  44059  cantnfresb  44168  omabs2  44176  fvnonrel  44440  rclexi  44458  rtrclex  44460  trclexi  44463  rtrclexi  44464  clcnvlem  44466  cnvrcl0  44468  cnvtrcl0  44469  dfrtrcl5  44472  dfrcl2  44517  comptiunov2i  44549  corclrcl  44550  trclrelexplem  44554  relexpaddss  44561  cotrcltrcl  44568  corcltrcl  44582  cotrclrcl  44585  frege131d  44607  0he  44625  grumnudlem  45112  uzmptshftfval  45173  binomcxplemdvbinom  45180  binomcxplemdvsum  45182  binomcxplemnotnn0  45183  modelaxreplem2  45805  rabexgf  45861  uzct  45900  disjf1o  46026  dmmptssf  46064  mptssid  46073  uzfissfz  46159  ssuzfz  46182  uzssre2  46238  uzublem  46261  uzssz2  46287  uzsscn2  46308  sumnnodd  46463  climconstmpt  46489  fnlimfvre  46505  fnlimabslt  46510  limsupubuzlem  46543  limsupubuz  46544  limsupequzmpt2  46549  limsupmnfuzlem  46557  limsupre3uzlem  46566  liminfequzmpt2  46622  ibliooicc  46802  stoweidlem44  46875  stoweidlem50  46881  stoweidlem51  46882  stoweidlem52  46883  stoweidlem57  46888  stoweidlem59  46890  fourierdlem16  46954  fourierdlem19  46957  fourierdlem21  46959  fourierdlem22  46960  fourierdlem42  46980  fourierdlem83  47020  fouriersw  47062  salexct  47165  salexct3  47173  salgencntex  47174  salgensscntex  47175  sge0less  47223  sge0fodjrnlem  47247  sge0isum  47258  ovnlerp  47393  ovn0lem  47396  hoidmv1lelem1  47422  hoidmv1lelem3  47424  hoidmvlelem1  47426  hoidmvlelem2  47427  hoidmvlelem3  47428  hoidmvlelem4  47429  ovnhoilem1  47432  ovnhoilem2  47433  opnvonmbllem2  47464  ovolval4lem1  47480  ovolval5lem3  47485  pimdecfgtioc  47546  pimincfltioc  47547  pimdecfgtioo  47548  pimincfltioo  47549  incsmflem  47572  decsmflem  47597  smflimlem2  47603  smflimlem3  47604  smflim  47608  smfrec  47620  smfmullem4  47625  smfdiv  47628  smfsuplem1  47642  smfsuplem3  47644  smfsupxr  47647  smfliminflem  47661  cfsetssfset  47947  fcoreslem2  47955  fcores  47958  gricrel  48838  clnbgrisubgrgrim  48851  isubgr3stgrlem6  48890  isubgr3stgrlem7  48891  isubgr3stgrlem8  48892  isubgr3stgr  48894  grlimgrtrilem2  48921  grlicrel  48925  oddibas  49091  2zlidl  49158  2zrngbas  49160  2zrng0  49162  fldcALTV  49250  fldhmsubcALTV  49251  dmtposss  49805  tposres3  49810  ipolub0  49921  imaidfu  50039