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 231	1 ⊢ 𝐴 ⊆ 𝐶

Syntax hints:   = wceq 1541   ⊆ wss 3898

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2725  df-ss 3915

This theorem is referenced by:  eqsstrri  3978  3sstr4i  3982  ssrab3  4031  rabssab  4034  ifssun  4494  opabss  5159  brab2a  5714  relopabiALT  5769  dmopabss  5864  rnopabss  5901  resss  5957  relres  5961  rnin  6101  rnxpss  6127  cnvcnvss  6149  resdmss  6190  resssxp  6225  dfpo2  6251  predss  6264  fnres  6616  f0  6712  nfvres  6869  fvopab4ndm  6968  ffvresb  7067  mptexgf  7165  funiunfv  7191  isoini2  7282  ovssunirn  7391  dmoprabss  7459  mpondm0  7595  elmpocl  7596  exse2  7856  fabexgOLD  7878  frxp  8065  tposssxp  8169  dftpos4  8184  smores  8281  smores2  8283  iordsmo  8286  swoer  8662  swoord1  8663  swoord2  8664  ecss  8682  ecopovsym  8752  ecopovtrn  8753  ecopover  8754  f1setex  8790  sbthlem7  9017  imafi  9210  elfiun  9325  marypha1lem  9328  marypha2lem1  9330  hartogslem1  9439  wdomima2g  9483  inf3lem1  9529  dmttrcl  9622  rnttrcl  9623  tc2  9641  frmin  9653  frrlem16  9662  frr1  9663  tz9.12lem1  9691  rankuni  9767  rankuniss  9770  rankmapu  9782  hta  9801  r0weon  9914  infxpenlem  9915  ackbij1lem9  10129  ackbij1lem10  10130  ackbij1b  10140  sdom2en01  10204  fin23lem26  10227  fin56  10295  fin1a2lem9  10310  axdc3lem  10352  axdc3lem2  10353  axcclem  10359  imadomg  10436  iundom2g  10442  smobeth  10488  canth4  10549  gruina  10720  grur1a  10721  pinn  10780  niex  10783  ltsopi  10790  ltrelpi  10791  dmaddpi  10792  dmmulpi  10793  enqex  10824  ltrelnq  10828  nqerf  10832  nqerrel  10834  dmrecnq  10870  lterpq  10872  ltrelpr  10900  enrex  10969  ltrelsr  10970  dmaddsr  10987  dmmulsr  10988  ltrelre  11036  axaddf  11047  axmulf  11048  ltrelxr  11184  lerelxr  11186  nn0ssre  12396  nn0sscn  12397  nn0ssz  12502  uzsupss  12844  rpnnen1lem1  12882  rpnnen1lem3  12883  rpnnen1lem5  12885  fz1ssfz0  13530  uzsup  13774  fzfi  13886  swrd00  14559  01sqrexlem3  15158  cau3  15270  caubnd  15273  limsupgre  15395  rlimpm  15414  rlimclim  15460  isercolllem1  15579  isercolllem2  15580  isercoll  15582  caurcvg  15591  caucvg  15593  iseraltlem2  15597  iseraltlem3  15598  zsum  15632  fsumcvg3  15643  climfsum  15734  ackbijnn  15742  divcnvshft  15769  infcvgaux1i  15771  clim2prod  15802  ntrivcvg  15811  ntrivcvgfvn0  15813  ntrivcvgtail  15814  ntrivcvgmullem  15815  ntrivcvgmul  15816  zprod  15851  dvdszrcl  16175  4sqlem1  16867  4sqlem19  16882  ramub1lem2  16946  structcnvcnv  17071  strleun  17075  fvsetsid  17086  smndex1sgrp  18824  gicer  19197  cntzsgrpcl  19254  symgbasfi  19299  mvdco  19365  symgsssg  19387  efglem  19636  efgtf  19642  efgtlen  19646  efginvrel2  19647  efginvrel1  19648  efgsfo  19659  efgredlemg  19662  efgredleme  19663  efgredlemd  19664  efgredlemc  19665  efgredlem  19667  efgred  19668  efgrelexlemb  19670  efgcpbllemb  19675  frgpinv  19684  frgpuplem  19692  frgpupf  19693  frgpup1  19695  frgpnabllem2  19794  gsumval3lem1  19825  gsumval3lem2  19826  gsumval3  19827  fldc  20708  fldhmsubc  20709  lbsextlem3  21106  pzriprnglem10  21436  znf1o  21497  zntoslem  21502  pjpm  21654  mhp0cl  22080  ply1bascl  22135  dmtopon  22858  ordtbas  23127  leordtval2  23147  lecldbas  23154  lmfval  23167  lmbrf  23195  cnconst2  23218  conncompcld  23369  hauspwdom  23436  txuni2  23500  xkouni  23534  xkoccn  23554  txkgen  23587  qtoptop2  23634  kqdisj  23667  hmphtop  23713  hmpher  23719  uzrest  23832  uzfbas  23833  lmflf  23940  tgpconncompeqg  24047  tgpconncomp  24048  ustn0  24156  xmeter  24368  isngp2  24532  xrtgioo  24742  iccntr  24757  xmetdcn  24774  metdcn  24776  metdscn2  24793  icchmeoOLD  24886  cnheiborlem  24900  reparphti  24943  lmmbrf  25209  iscau4  25226  iscauf  25227  caucfil  25230  lmclimf  25251  volf  25477  uniioombllem3  25533  uniioombllem4  25534  uniioombllem5  25535  volcn  25554  mbfimaopnlem  25603  mbflimsup  25614  i1f1  25638  itg2lcl  25675  itgioo  25764  itgsplitioo  25786  limcflflem  25828  limcflf  25829  limcresi  25833  lhop  25968  dvfsumlem1  25979  dvfsumlem2  25980  dvfsumlem2OLD  25981  dvfsumlem3  25982  dvfsumlem4  25983  dvfsumrlimge0  25984  dvfsumrlim  25985  dvfsumrlim2  25986  dvfsum2  25988  vieta1lem1  26265  vieta1lem2  26266  psercnlem2  26381  psercnlem1  26382  psercn  26383  pserdvlem1  26384  pserdvlem2  26385  pserdv  26386  pserdv2  26387  logcnlem5  26602  dvlog  26607  dvlog2lem  26608  dvlog2  26609  dvcncxp1  26699  dvcnsqrt  26700  cxpcn3lem  26704  cxpcn3  26705  sqrtcn  26707  1cubr  26799  atansssdm  26890  jensen  26946  musum  27148  ppiub  27162  lgsquadlem1  27338  lgsquadlem2  27339  lgsquadlem3  27340  2sqlem7  27382  nosupbnd1lem1  27667  nosupbnd2  27675  noinfbnd1lem1  27682  scutf  27773  leftssold  27844  rightssold  27845  mulsproplem12  28086  mulsproplem13  28087  mulsproplem14  28088  precsexlem8  28172  onssno  28211  nnssn0s  28270  dfnns2  28317  axtgcgrrflx  28460  axtgcgrid  28461  axtgsegcon  28462  axtg5seg  28463  axtgbtwnid  28464  axtgpasch  28465  axtgcont1  28466  tglng  28544  disjxwwlkn  29912  frgrwopreg2  30320  phnv  30815  htthlem  30918  hlimadd  31194  hlimcaui  31237  hhsscms  31279  occllem  31304  shjshsi  31493  3oalem4  31666  pjfi  31705  dmadjss  31888  nlelshi  32061  nlelchi  32062  hmopidmchi  32152  shatomistici  32362  difxp1ss  32523  difxp2ss  32524  fcoinver  32605  opabssi  32617  mptctf  32723  ccatws1f1o  32961  gsumpart  33074  pmtrcnel2  33100  psgnfzto1stlem  33110  cycpmrn  33153  cyc3genpm  33162  unitprodclb  33398  lsmsnorb  33400  ply1degltel  33603  ply1degleel  33604  ply1degltlss  33605  evlextv  33635  vietalem  33663  constrsscn  33825  cnre2csqima  33996  raddcn  34014  zrhcntr  34064  rrhre  34106  esumsnf  34149  sxbrsiga  34375  omssubadd  34385  carsggect  34403  sitmcl  34436  oddpwdc  34439  eulerpartlem1  34452  eulerpartlemt  34456  eulerpartgbij  34457  eulerpartlemmf  34460  eulerpartlemgh  34463  sseqf  34477  ballotlemfmpn  34580  ballotth  34623  signswch  34646  ftc2re  34683  fdvposlt  34684  fdvposle  34686  bnj1146  34875  bnj1292  34899  bnj1293  34900  bnj1145  35077  bnj1177  35090  tz9.1regs  35202  fineqvnttrclse  35216  erdszelem2  35308  kur14lem3  35324  kur14lem6  35327  kur14lem7  35328  kur14lem9  35330  cvmlift2lem12  35430  mpstssv  35655  mstapst  35663  mppspstlem  35687  mppspst  35690  mthmsta  35694  mthmpps  35698  mclsppslem  35699  txpss3v  35992  pprodss4v  35998  relsset  36002  fixssdm  36020  fixssrn  36021  limitssson  36025  funpartss  36060  colinearex  36176  fneer  36469  neibastop1  36475  neibastop2lem  36476  filnetlem2  36495  filnetlem3  36496  knoppcnlem10  36618  bj-tagss  37097  bj-imdirco  37307  bj-fvsnun2  37373  bj-ablssgrp  37393  bj-ablsscmn  37395  bj-vecssmod  37398  bj-fldssdrng  37405  icoreresf  37469  icoreunrn  37476  poimirlem29  37762  poimirlem30  37763  poimirlem31  37764  poimir  37766  broucube  37767  dvasin  37817  dvacos  37818  areacirc  37826  caures  37873  bnd2lem  37904  ismtyres  37921  flddivrng  38112  xrnss3v  38478  refrelsredund2  38802  toycom  39145  dihglblem2N  41466  lcdvbase  41765  mapdunirnN  41822  aks6d1c1p1rcl  42274  redvmptabs  42530  readvrec  42532  prjspreln0  42767  prjspvs  42768  prjspeclsp  42770  0prjspnrel  42785  dffltz  42792  eldiophb  42914  monotuz  43098  pwssplit4  43246  pwfi2f1o  43253  arearect  43372  cantnfresb  43481  omabs2  43489  fvnonrel  43754  rclexi  43772  rtrclex  43774  trclexi  43777  rtrclexi  43778  clcnvlem  43780  cnvrcl0  43782  cnvtrcl0  43783  dfrtrcl5  43786  dfrcl2  43831  comptiunov2i  43863  corclrcl  43864  trclrelexplem  43868  relexpaddss  43875  cotrcltrcl  43882  corcltrcl  43896  cotrclrcl  43899  frege131d  43921  0he  43939  grumnudlem  44442  uzmptshftfval  44503  binomcxplemdvbinom  44510  binomcxplemdvsum  44512  binomcxplemnotnn0  44513  modelaxreplem2  45136  rabexgf  45185  uzct  45224  disjf1o  45351  dmmptssf  45392  mptssid  45401  uzfissfz  45487  ssuzfz  45510  uzssre2  45567  uzublem  45590  uzssz2  45616  uzsscn2  45637  sumnnodd  45792  climconstmpt  45818  fnlimfvre  45834  fnlimabslt  45839  limsupvaluz  45868  limsupubuzlem  45872  limsupubuz  45873  limsupequzmpt2  45878  limsupmnfuzlem  45886  limsupre3uzlem  45895  liminfequzmpt2  45951  ibliooicc  46131  stoweidlem44  46204  stoweidlem50  46210  stoweidlem51  46211  stoweidlem52  46212  stoweidlem57  46217  stoweidlem59  46219  fourierdlem16  46283  fourierdlem19  46286  fourierdlem21  46288  fourierdlem22  46289  fourierdlem42  46309  fourierdlem83  46349  fouriersw  46391  salexct  46494  salexct3  46502  salgencntex  46503  salgensscntex  46504  sge0less  46552  sge0fodjrnlem  46576  sge0isum  46587  ovnlerp  46722  ovn0lem  46725  hoidmv1lelem1  46751  hoidmv1lelem3  46753  hoidmvlelem1  46755  hoidmvlelem2  46756  hoidmvlelem3  46757  hoidmvlelem4  46758  ovnhoilem1  46761  ovnhoilem2  46762  opnvonmbllem2  46793  ovolval4lem1  46809  ovolval5lem3  46814  pimdecfgtioc  46875  pimincfltioc  46876  pimdecfgtioo  46877  pimincfltioo  46878  incsmflem  46901  decsmflem  46926  smflimlem2  46932  smflimlem3  46933  smflim  46937  smfrec  46949  smfmullem4  46954  smfdiv  46957  smfsuplem1  46971  smfsuplem3  46973  smfsupxr  46976  smfliminflem  46990  cfsetssfset  47218  fcoreslem2  47226  fcores  47229  gricrel  48081  clnbgrisubgrgrim  48094  isubgr3stgrlem6  48133  isubgr3stgrlem7  48134  isubgr3stgrlem8  48135  isubgr3stgr  48137  grlimgrtrilem2  48164  grlicrel  48168  oddibas  48335  2zlidl  48402  2zrngbas  48404  2zrng0  48406  fldcALTV  48494  fldhmsubcALTV  48495  dmtposss  49037  tposres3  49042  ipolub0  49153  imaidfu  49271