Theorem eqsstri 3961

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 3943	. 2 ⊢ (𝐴 ⊆ 𝐶 ↔ 𝐵 ⊆ 𝐶)
4	1, 3	mpbir 232	1 ⊢ 𝐴 ⊆ 𝐶

Syntax hints:   = wceq 1547   ⊆ wss 3883

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-cleq 2731  df-ss 3900

This theorem is referenced by:  eqsstrri  3962  3sstr4i  3966  ssrab3  4014  rabssab  4017  ifssun  4473  opabss  5137  brab2a  5712  relopabiALT  5767  dmopabss  5861  rnopabss  5898  resss  5954  relres  5958  rnin  6098  rnxpss  6124  cnvcnvss  6146  resdmss  6187  resssxp  6222  dfpo2  6248  predss  6261  fnres  6613  f0  6709  nfvres  6866  fvopab4ndm  6967  ffvresb  7068  mptexgf  7167  funiunfv  7193  isoini2  7284  ovssunirn  7393  dmoprabss  7461  mpondm0  7597  elmpocl  7598  exse2  7858  fabexgOLD  7880  frxp  8067  tposssxp  8171  dftpos4  8186  smores  8283  smores2  8285  iordsmo  8288  swoer  8666  swoord1  8667  swoord2  8668  ecss  8686  ecopovsym  8757  ecopovtrn  8758  ecopover  8759  f1setex  8795  sbthlem7  9022  imafi  9216  elfiun  9334  marypha1lem  9337  marypha2lem1  9339  hartogslem1  9448  wdomima2g  9492  inf3lem1  9541  dmttrcl  9634  rnttrcl  9635  tc2  9653  frmin  9665  frrlem16  9674  frr1  9675  tz9.12lem1  9703  rankuni  9779  rankuniss  9782  rankmapu  9794  hta  9813  r0weon  9926  infxpenlem  9927  ackbij1lem9  10141  ackbij1lem10  10142  ackbij1b  10152  sdom2en01  10216  fin23lem26  10239  fin56  10307  fin1a2lem9  10322  axdc3lem  10364  axdc3lem2  10365  axcclem  10371  imadomg  10448  iundom2g  10454  smobeth  10501  canth4  10562  gruina  10733  grur1a  10734  pinn  10793  niex  10796  ltsopi  10803  ltrelpi  10804  dmaddpi  10805  dmmulpi  10806  enqex  10837  ltrelnq  10841  nqerf  10845  nqerrel  10847  dmrecnq  10883  lterpq  10885  ltrelpr  10913  enrex  10982  ltrelsr  10983  dmaddsr  11000  dmmulsr  11001  ltrelre  11049  axaddf  11060  axmulf  11061  ltrelxr  11198  lerelxr  11200  nn0ssre  12433  nn0sscn  12434  nn0ssz  12539  uzsupss  12882  rpnnen1lem1  12920  rpnnen1lem3  12921  rpnnen1lem5  12923  fz1ssfz0  13569  uzsup  13814  fzfi  13926  swrd00  14599  01sqrexlem3  15198  cau3  15310  caubnd  15313  limsupgre  15435  rlimpm  15454  rlimclim  15500  isercolllem1  15619  isercolllem2  15620  isercoll  15622  caurcvg  15631  caucvg  15633  iseraltlem2  15637  iseraltlem3  15638  zsum  15672  fsumcvg3  15683  climfsum  15775  ackbijnn  15785  divcnvshft  15812  infcvgaux1i  15814  clim2prod  15845  ntrivcvg  15854  ntrivcvgfvn0  15856  ntrivcvgtail  15857  ntrivcvgmullem  15858  ntrivcvgmul  15859  zprod  15894  dvdszrcl  16218  4sqlem1  16911  4sqlem19  16926  ramub1lem2  16990  structcnvcnv  17115  strleun  17119  fvsetsid  17130  smndex1sgrp  18871  gicer  19244  cntzsgrpcl  19301  symgbasfi  19346  mvdco  19412  symgsssg  19434  efglem  19683  efgtf  19689  efgtlen  19693  efginvrel2  19694  efginvrel1  19695  efgsfo  19706  efgredlemg  19709  efgredleme  19710  efgredlemd  19711  efgredlemc  19712  efgredlem  19714  efgred  19715  efgrelexlemb  19717  efgcpbllemb  19722  frgpinv  19731  frgpuplem  19739  frgpupf  19740  frgpup1  19742  frgpnabllem2  19841  gsumval3lem1  19872  gsumval3lem2  19873  gsumval3  19874  fldc  20757  fldhmsubc  20758  lbsextlem3  21154  pzriprnglem10  21466  znf1o  21527  zntoslem  21532  pjpm  21684  mhp0cl  22135  ply1bascl  22189  dmtopon  22907  ordtbas  23176  leordtval2  23196  lecldbas  23203  lmfval  23216  lmbrf  23244  cnconst2  23267  conncompcld  23418  hauspwdom  23485  txuni2  23549  xkouni  23583  xkoccn  23603  txkgen  23636  qtoptop2  23683  kqdisj  23716  hmphtop  23762  hmpher  23768  uzrest  23881  uzfbas  23882  lmflf  23989  tgpconncompeqg  24096  tgpconncomp  24097  ustn0  24205  xmeter  24417  isngp2  24581  xrtgioo  24791  iccntr  24806  xmetdcn  24823  metdcn  24825  metdscn2  24842  cnheiborlem  24940  reparphti  24983  lmmbrf  25248  iscau4  25265  iscauf  25266  caucfil  25269  lmclimf  25290  volf  25515  uniioombllem3  25571  uniioombllem4  25572  uniioombllem5  25573  volcn  25592  mbfimaopnlem  25641  mbflimsup  25652  i1f1  25676  itg2lcl  25713  itgioo  25802  itgsplitioo  25824  limcflflem  25866  limcflf  25867  limcresi  25871  lhop  26002  dvfsumlem1  26012  dvfsumlem2  26013  dvfsumlem3  26014  dvfsumlem4  26015  dvfsumrlimge0  26016  dvfsumrlim  26017  dvfsumrlim2  26018  dvfsum2  26020  vieta1lem1  26295  vieta1lem2  26296  psercnlem2  26408  psercnlem1  26409  psercn  26410  pserdvlem1  26411  pserdvlem2  26412  pserdv  26413  pserdv2  26414  logcnlem5  26629  dvlog  26634  dvlog2lem  26635  dvlog2  26636  dvcncxp1  26726  dvcnsqrt  26727  cxpcn3lem  26730  cxpcn3  26731  sqrtcn  26733  1cubr  26825  atansssdm  26916  jensen  26971  musum  27173  ppiub  27186  lgsquadlem1  27362  lgsquadlem2  27363  lgsquadlem3  27364  2sqlem7  27406  nosupbnd1lem1  27691  nosupbnd2  27699  noinfbnd1lem1  27706  cutsf  27803  leftssold  27882  rightssold  27883  mulsproplem12  28138  mulsproplem13  28139  mulsproplem14  28140  precsexlem8  28225  onssno  28265  nnssn0s  28332  dfnns2  28383  bdaypw2n0bndlem  28474  axtgcgrrflx  28549  axtgcgrid  28550  axtgsegcon  28551  axtg5seg  28552  axtgbtwnid  28553  axtgpasch  28554  axtgcont1  28555  tglng  28633  disjxwwlkn  30000  frgrwopreg2  30408  phnv  30904  htthlem  31007  hlimadd  31283  hlimcaui  31326  hhsscms  31368  occllem  31393  shjshsi  31582  3oalem4  31755  pjfi  31794  dmadjss  31977  nlelshi  32150  nlelchi  32151  hmopidmchi  32241  shatomistici  32451  difxp1ss  32611  difxp2ss  32612  fcoinver  32694  opabssi  32706  mptctf  32809  ccatws1f1o  33031  gsumpart  33145  pmtrcnel2  33172  psgnfzto1stlem  33182  cycpmrn  33225  cyc3genpm  33234  unitprodclb  33473  lsmsnorb  33475  ply1degltel  33686  ply1degleel  33687  ply1degltlss  33688  evlextv  33735  vietalem  33772  constrsscn  33933  cnre2csqima  34104  raddcn  34122  zrhcntr  34172  rrhre  34214  esumsnf  34257  sxbrsiga  34483  omssubadd  34493  carsggect  34511  sitmcl  34544  oddpwdc  34547  eulerpartlem1  34560  eulerpartlemt  34564  eulerpartgbij  34565  eulerpartlemmf  34568  eulerpartlemgh  34571  sseqf  34585  ballotlemfmpn  34688  ballotth  34731  signswch  34754  ftc2re  34791  fdvposlt  34792  fdvposle  34794  bnj1146  34982  bnj1292  35006  bnj1293  35007  bnj1145  35184  bnj1177  35197  fineqvnttrclse  35314  tz9.1regs  35324  erdszelem2  35429  kur14lem3  35445  kur14lem6  35448  kur14lem7  35449  kur14lem9  35451  cvmlift2lem12  35551  mpstssv  35776  mstapst  35784  mppspstlem  35808  mppspst  35811  mthmsta  35815  mthmpps  35819  mclsppslem  35820  txpss3v  36113  pprodss4v  36119  relsset  36123  fixssdm  36141  fixssrn  36142  limitssson  36146  funpartss  36181  colinearex  36297  fneer  36590  neibastop1  36596  neibastop2lem  36597  filnetlem2  36616  filnetlem3  36617  ttcuniun  36747  ttcuni  36750  knoppcnlem10  36817  bj-tagss  37342  bj-imdirco  37559  bj-fvsnun2  37625  bj-ablssgrp  37645  bj-ablsscmn  37647  bj-vecssmod  37650  bj-fldssdrng  37657  icoreresf  37723  icoreunrn  37730  poimirlem29  38025  poimirlem30  38026  poimirlem31  38027  poimir  38029  broucube  38030  dvasin  38080  dvacos  38081  areacirc  38089  caures  38136  bnd2lem  38167  ismtyres  38184  flddivrng  38375  xrnss3v  38757  refrelsredund2  39093  toycom  39474  dihglblem2N  41795  lcdvbase  42094  mapdunirnN  42151  aks6d1c1p1rcl  42602  redvmptabs  42846  readvrec  42848  prjspreln0  43068  prjspvs  43069  prjspeclsp  43071  0prjspnrel  43086  dffltz  43093  eldiophb  43215  monotuz  43395  pwssplit4  43543  pwfi2f1o  43550  arearect  43669  cantnfresb  43778  omabs2  43786  fvnonrel  44050  rclexi  44068  rtrclex  44070  trclexi  44073  rtrclexi  44074  clcnvlem  44076  cnvrcl0  44078  cnvtrcl0  44079  dfrtrcl5  44082  dfrcl2  44127  comptiunov2i  44159  corclrcl  44160  trclrelexplem  44164  relexpaddss  44171  cotrcltrcl  44178  corcltrcl  44192  cotrclrcl  44195  frege131d  44217  0he  44235  grumnudlem  44738  uzmptshftfval  44799  binomcxplemdvbinom  44806  binomcxplemdvsum  44808  binomcxplemnotnn0  44809  modelaxreplem2  45432  rabexgf  45481  uzct  45520  disjf1o  45646  dmmptssf  45684  mptssid  45693  uzfissfz  45779  ssuzfz  45802  uzssre2  45858  uzublem  45881  uzssz2  45907  uzsscn2  45928  sumnnodd  46083  climconstmpt  46109  fnlimfvre  46125  fnlimabslt  46130  limsupvaluz  46159  limsupubuzlem  46163  limsupubuz  46164  limsupequzmpt2  46169  limsupmnfuzlem  46177  limsupre3uzlem  46186  liminfequzmpt2  46242  ibliooicc  46422  stoweidlem44  46495  stoweidlem50  46501  stoweidlem51  46502  stoweidlem52  46503  stoweidlem57  46508  stoweidlem59  46510  fourierdlem16  46574  fourierdlem19  46577  fourierdlem21  46579  fourierdlem22  46580  fourierdlem42  46600  fourierdlem83  46640  fouriersw  46682  salexct  46785  salexct3  46793  salgencntex  46794  salgensscntex  46795  sge0less  46843  sge0fodjrnlem  46867  sge0isum  46878  ovnlerp  47013  ovn0lem  47016  hoidmv1lelem1  47042  hoidmv1lelem3  47044  hoidmvlelem1  47046  hoidmvlelem2  47047  hoidmvlelem3  47048  hoidmvlelem4  47049  ovnhoilem1  47052  ovnhoilem2  47053  opnvonmbllem2  47084  ovolval4lem1  47100  ovolval5lem3  47105  pimdecfgtioc  47166  pimincfltioc  47167  pimdecfgtioo  47168  pimincfltioo  47169  incsmflem  47192  decsmflem  47217  smflimlem2  47223  smflimlem3  47224  smflim  47228  smfrec  47240  smfmullem4  47245  smfdiv  47248  smfsuplem1  47262  smfsuplem3  47264  smfsupxr  47267  smfliminflem  47281  cfsetssfset  47527  fcoreslem2  47535  fcores  47538  gricrel  48418  clnbgrisubgrgrim  48431  isubgr3stgrlem6  48470  isubgr3stgrlem7  48471  isubgr3stgrlem8  48472  isubgr3stgr  48474  grlimgrtrilem2  48501  grlicrel  48505  oddibas  48672  2zlidl  48739  2zrngbas  48741  2zrng0  48743  fldcALTV  48831  fldhmsubcALTV  48832  dmtposss  49374  tposres3  49379  ipolub0  49490  imaidfu  49608