Theorem eqsstri 3843

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

Syntax hints:   = wceq 1637   ⊆ wss 3780

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2069  ax-7 2105  ax-9 2166  ax-10 2186  ax-11 2202  ax-12 2215  ax-ext 2795

This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2062  df-clab 2804  df-cleq 2810  df-clel 2813  df-in 3787  df-ss 3794

This theorem is referenced by:  eqsstr3i  3844  ssrab2  3895  ssrab3  3896  rabssab  3899  opabss  4919  brab2a  5410  relopabiALT  5462  dmopabss  5551  resss  5639  relres  5643  rnin  5767  rnxpss  5791  cnvcnvss  5814  dmmptss  5859  predss  5914  fnres  6228  f0  6311  nfvres  6454  fvopab4ndm  6538  ffvresb  6626  mptexgf  6720  funiunfv  6740  isoini2  6823  ovssunirn  6919  dmoprabss  6982  mpt2ndm0  7115  elmpt2cl  7116  omsson  7309  exse2  7345  fabexg  7362  frxp  7531  tposssxp  7601  dftpos4  7616  wfrdmss  7667  smores  7695  smores2  7697  iordsmo  7700  oawordeulem  7881  swoer  8019  swoord1  8020  swoord2  8021  ecss  8033  ecopovsym  8095  ecopovtrn  8096  ecopover  8097  sbthlem7  8325  nnfi  8402  imafi  8508  elfiun  8585  marypha1lem  8588  marypha2lem1  8590  ordtypelem2  8673  hartogslem1  8696  wemapso2lem  8706  wdomima2g  8740  inf3lem1  8782  wemapwe  8851  tc2  8875  tz9.12lem1  8907  rankuni  8983  rankuniss  8986  rankmapu  8998  cplem1  9009  hta  9017  r0weon  9128  infxpenlem  9129  ackbij1lem9  9345  ackbij1lem10  9346  ackbij1b  9356  cofsmo  9386  sdom2en01  9419  fin23lem26  9442  fin23lem28  9457  fin23lem30  9459  isf32lem5  9474  isf32lem6  9475  isf32lem7  9476  isf32lem8  9477  fin56  9510  fin1a2lem9  9525  hsmexlem4  9546  hsmexlem5  9547  hsmexlem6  9548  axdc3lem  9567  axdc3lem2  9568  axcclem  9574  zorn2lem1  9613  zorn2lem3  9615  zorn2lem4  9616  zorn2lem5  9617  imadomg  9651  iundom2g  9657  smobeth  9703  canth4  9764  gruina  9935  grur1a  9936  pinn  9995  niex  9998  ltsopi  10005  ltrelpi  10006  dmaddpi  10007  dmmulpi  10008  enqex  10039  0nnq  10041  elpqn  10042  ltrelnq  10043  nqerf  10047  nqerrel  10049  dmrecnq  10085  lterpq  10087  ltrelpr  10115  enrex  10183  ltrelsr  10184  dmaddsr  10201  dmmulsr  10202  ltrelre  10250  axaddf  10261  axmulf  10262  ltrelxr  10394  lerelxr  10396  nn0ssre  11583  nn0ssz  11684  uzsupss  12019  rpnnen1lem2  12053  rpnnen1lem1  12054  rpnnen1lem3  12055  rpnnen1lem5  12057  rpre  12073  fz1ssfz0  12679  uzsup  12906  fzfi  13015  swrd00  13661  sqrlem3  14228  sqrlem5  14230  cau3  14338  caubnd  14341  limsupgre  14455  rlimpm  14474  rlimclim  14520  isercolllem1  14638  isercolllem2  14639  isercoll  14641  caurcvg  14650  caucvg  14652  iseraltlem2  14656  iseraltlem3  14657  zsum  14692  fsumcvg3  14703  climfsum  14794  ackbijnn  14802  divcnvshft  14829  infcvgaux1i  14831  clim2prod  14861  ntrivcvg  14870  ntrivcvgfvn0  14872  ntrivcvgtail  14873  ntrivcvgmullem  14874  ntrivcvgmul  14875  zprod  14908  dvdszrcl  15228  dvdsflip  15282  divalglem2  15358  divalglem5  15360  divalglem8  15363  gcdcllem3  15462  bezoutlem2  15496  bezoutlem3  15497  maxprmfct  15658  phimullem  15721  eulerthlem2  15724  pclem  15780  infpn2  15854  prmreclem2  15858  prmreclem3  15859  prmreclem5  15861  4sqlem1  15889  4sqlem13  15898  4sqlem14  15899  4sqlem17  15902  4sqlem18  15903  4sqlem19  15904  vdwnnlem3  15938  ramcl2lem  15950  ramtcl  15951  ramtcl2  15952  ramtub  15953  ramub1lem2  15968  structcnvcnv  16102  fvsetsid  16121  strlemor0OLD  16199  strlemor1OLD  16200  strleun  16203  imasdsval2  16401  gsumval1  17502  nmzsubg  17857  nmznsg  17860  conjnmz  17916  conjnmzb  17917  gicer  17940  gastacl  17963  symgbasfi  18027  mvdco  18086  symgsssg  18108  sylow1lem2  18235  sylow1lem3  18236  sylow1lem4  18237  sylow1lem5  18238  sylow2a  18255  sylow3lem2  18264  efglem  18350  efgtf  18356  efgtlen  18360  efginvrel2  18361  efginvrel1  18362  efgsfo  18373  efgredlemg  18376  efgredleme  18377  efgredlemd  18378  efgredlemc  18379  efgredlem  18381  efgred  18382  efgrelexlemb  18384  efgcpbllemb  18389  frgpinv  18398  frgpuplem  18406  frgpupf  18407  frgpup1  18409  frgpnabllem2  18498  gsumval3lem1  18527  gsumval3lem2  18528  gsumval3  18529  ablfacrplem  18686  ablfacrp2  18688  ablfac1eu  18694  pgpfaclem1  18702  ablfaclem2  18707  ablfaclem3  18708  lspsolvlem  19370  lbsextlem2  19388  lbsextlem3  19389  lbsextlem4  19390  rrgeq0  19519  rrgss  19521  psrbagconf1o  19603  psrass1lem  19606  mplbasss  19661  ply1bascl  19801  coe1mul2lem2  19866  znf1o  20127  zntoslem  20132  cygznlem2a  20143  psgnghm  20153  pjpm  20283  dsmmbase  20310  frlmsslsp  20366  dmtopon  20962  mretopd  21131  ordtbas  21231  leordtval2  21251  lecldbas  21258  lmfval  21271  lmbrf  21299  cnconst2  21322  hauscmplem  21444  conncompcld  21472  hauspwdom  21539  txuni2  21603  xkouni  21637  xkoccn  21657  txkgen  21690  qtoptop2  21737  kqdisj  21770  hmphtop  21816  hmpher  21822  uzrest  21935  uzfbas  21936  lmflf  22043  ptcmplem1  22090  ptcmplem3  22092  tgpconncompeqg  22149  tgpconncomp  22150  ustn0  22258  imasdsf1olem  22412  xmeter  22472  blcld  22544  isngp2  22635  xrtgioo  22843  iccntr  22858  icccmplem1  22859  icccmplem2  22860  icccmplem3  22861  xmetdcn  22875  metdcn  22877  metdscn2  22894  icchmeo  22974  cnheiborlem  22987  lmmbrf  23294  iscau4  23311  iscauf  23312  caucfil  23315  lmclimf  23336  rrxf  23419  ivthlem1  23455  ivthlem2  23456  ivthlem3  23457  ovolsslem  23488  ovolicc2lem3  23523  ovolicc2lem4  23524  ovolicc2lem5  23525  ovolicc2  23526  volf  23533  uniioombllem3  23589  uniioombllem4  23590  uniioombllem5  23591  dyadmbllem  23603  dyadmbl  23604  volcn  23610  mbfimaopnlem  23659  mbflimsup  23670  i1f1  23694  itg2lcl  23731  iblmbf  23771  itgioo  23819  itgsplitioo  23841  limcflflem  23881  limcflf  23882  limcresi  23886  lhop  24016  dvfsumlem1  24026  dvfsumlem2  24027  dvfsumlem3  24028  dvfsumlem4  24029  dvfsumrlimge0  24030  dvfsumrlim  24031  dvfsumrlim2  24032  dvfsum2  24034  vieta1lem1  24302  vieta1lem2  24303  psercnlem2  24415  psercnlem1  24416  psercn  24417  pserdvlem1  24418  pserdvlem2  24419  pserdv  24420  pserdv2  24421  abelthlem4  24425  abelthlem6  24427  abelthlem9  24431  abelth  24432  logcnlem5  24629  dvlog  24634  dvlog2lem  24635  dvlog2  24636  dvcncxp1  24721  dvcnsqrt  24722  cxpcn3lem  24725  cxpcn3  24726  sqrtcn  24728  1cubr  24806  atansssdm  24897  atancn  24900  jensen  24952  lgamucov  25001  lgamucov2  25002  ftalem3  25038  musum  25154  dvdsmulf1o  25157  fsumdvdsmul  25158  ppiub  25166  lgsfcl2  25265  lgsquadlem1  25342  lgsquadlem2  25343  lgsquadlem3  25344  2sqlem7  25386  rpvmasum2  25438  dchrisum0re  25439  dchrisum0lema  25440  dchrisum0lem1b  25441  dchrisum0lem1  25442  dchrisum0lem2a  25443  dchrisum0lem2  25444  dchrisum0lem3  25445  dchrisum0  25446  pntlem3  25535  axtgcgrrflx  25598  axtgcgrid  25599  axtgsegcon  25600  axtg5seg  25601  axtgbtwnid  25602  axtgpasch  25603  axtgcont1  25604  tglng  25678  axcontlem2  26082  axcontlem7  26087  axcontlem8  26088  axcontlem10  26090  upgrreslem  26435  umgrreslem  26436  vtxdginducedm1lem2  26687  finsumvtxdg2ssteplem1  26692  disjxwwlkn  27074  clwwlknclwwlkdifnumOLD  27146  clwwlksswrd  27153  frgrwopreg2  27517  phnv  28020  htthlem  28125  hlimadd  28401  hlimcaui  28444  hhsscms  28487  occllem  28513  shjshsi  28702  3oalem4  28875  pjfi  28914  dmadjss  29097  nlelshi  29270  nlelchi  29271  hmopidmchi  29361  atssch  29553  shatomistici  29571  fcoinver  29766  opabssi  29773  mptctf  29845  fcobijfs  29851  psgnfzto1stlem  30198  cnre2csqima  30305  raddcn  30323  rrhre  30413  esumsnf  30474  sxbrsiga  30700  omssubadd  30710  carsggect  30728  sitmcl  30761  oddpwdc  30764  eulerpartlem1  30777  eulerpartlemt  30781  eulerpartgbij  30782  eulerpartlemmf  30785  eulerpartlemgh  30788  sseqf  30802  ballotlemfmpn  30904  ballotth  30947  signswch  30986  ftc2re  31024  fdvposlt  31025  fdvposle  31027  bnj1146  31207  bnj1292  31231  bnj1293  31232  bnj1145  31406  bnj1177  31419  subfacp1lem3  31509  subfacp1lem5  31511  erdszelem2  31519  kur14lem3  31535  kur14lem6  31538  kur14lem7  31539  kur14lem9  31541  cvmlift2lem12  31641  mpstssv  31781  mstapst  31789  mppspstlem  31813  mppspst  31816  mthmsta  31820  mthmpps  31824  mclsppslem  31825  dfpo2  31989  wlimss  32117  frrlem7  32133  nosupbnd1lem1  32197  nosupbnd2  32205  scutf  32262  txpss3v  32328  pprodss4v  32334  relsset  32338  fixssdm  32356  fixssrn  32357  limitssson  32361  funpartss  32394  colinearex  32510  fneer  32691  neibastop1  32697  neibastop2lem  32698  filnetlem2  32717  filnetlem3  32718  knoppcnlem10  32831  bj-tagss  33297  bj-cmnssmnd  33472  bj-ablssgrp  33474  bj-ablsscmn  33476  bj-vecssmod  33479  bj-rrvecssvec  33486  icoreresf  33535  icoreunrn  33542  cnfinltrel  33576  poimirlem29  33770  poimirlem30  33771  poimirlem31  33772  poimir  33774  broucube  33775  dvasin  33827  dvacos  33828  areacirc  33836  caures  33886  bnd2lem  33920  ismtyres  33937  flddivrng  34128  xrnss3v  34466  toycom  34772  dihglblem2N  37093  lcdvbase  37392  mapdunirnN  37449  eldiophb  37840  monotuz  38025  fglmod  38162  pwssplit4  38178  pwfi2f1o  38185  arearect  38319  fvnonrel  38421  rclexi  38440  rtrclex  38442  trclexi  38445  rtrclexi  38446  clcnvlem  38448  cnvrcl0  38450  cnvtrcl0  38451  dfrtrcl5  38454  dfrcl2  38484  comptiunov2i  38516  corclrcl  38517  trclrelexplem  38521  relexpaddss  38528  cotrcltrcl  38535  corcltrcl  38549  cotrclrcl  38552  frege131d  38574  rp-imass  38583  0he  38594  uzmptshftfval  39063  binomcxplemdvbinom  39070  binomcxplemdvsum  39072  binomcxplemnotnn0  39073  rabexgf  39695  uzct  39743  disjf1o  39885  dmresss  39938  dmmptssf  39940  mptssid  39952  uzfissfz  40040  ssuzfz  40063  uzssre2  40130  uzublem  40154  uzssz2  40182  uzsscn2  40205  sumnnodd  40360  climconstmpt  40388  fnlimfvre  40404  fnlimabslt  40409  limsupvaluz  40438  limsupubuzlem  40442  limsupubuz  40443  limsupequzmpt2  40448  limsupmnfuzlem  40456  limsupre3uzlem  40465  liminfequzmpt2  40521  ibliooicc  40684  stoweidlem44  40758  stoweidlem50  40764  stoweidlem51  40765  stoweidlem52  40766  stoweidlem57  40771  stoweidlem59  40773  fourierdlem16  40837  fourierdlem19  40840  fourierdlem21  40842  fourierdlem22  40843  fourierdlem42  40863  fourierdlem83  40903  fouriersw  40945  salexct  41049  salexct3  41057  salgencntex  41058  salgensscntex  41059  sge0less  41106  sge0fodjrnlem  41130  sge0isum  41141  ovnsslelem  41274  ovnlerp  41276  ovn0lem  41279  hoidmv1lelem1  41305  hoidmv1lelem3  41307  hoidmvlelem1  41309  hoidmvlelem2  41310  hoidmvlelem3  41311  hoidmvlelem4  41312  ovnhoilem1  41315  ovnhoilem2  41316  opnvonmbllem2  41347  ovolval4lem1  41363  ovolval5lem3  41368  pimdecfgtioc  41425  pimincfltioc  41426  pimdecfgtioo  41427  pimincfltioo  41428  incsmflem  41450  decsmflem  41474  smflimlem2  41480  smflimlem3  41481  smflim  41485  smfrec  41496  smfmullem4  41501  smfdiv  41504  smfsuplem1  41517  smfsuplem3  41519  smfsupxr  41522  smfliminflem  41536  oddibas  42399  2zlidl  42520  2zrngbas  42522  2zrng0  42524  fldc  42669  fldhmsubc  42670  fldcALTV  42687  fldhmsubcALTV  42688  setrec2lem1  43026