Theorem eqsstri 3886

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

Syntax hints:   = wceq 1508   ⊆ wss 3824

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1759  ax-4 1773  ax-5 1870  ax-6 1929  ax-7 1966  ax-8 2053  ax-9 2060  ax-10 2080  ax-11 2094  ax-12 2107  ax-ext 2745

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 835  df-tru 1511  df-ex 1744  df-nf 1748  df-sb 2017  df-clab 2754  df-cleq 2766  df-clel 2841  df-in 3831  df-ss 3838

This theorem is referenced by:  eqsstr3i  3887  ssrab2  3941  ssrab3  3942  rabssab  3945  opabss  4990  brab2a  5491  relopabiALT  5542  dmopabss  5632  resss  5721  relres  5725  rnin  5843  rnxpss  5867  cnvcnvss  5889  predss  5991  fnres  6304  f0  6387  nfvres  6534  fvopab4ndm  6621  ffvresb  6710  mptexgf  6810  funiunfv  6831  isoini2  6914  ovssunirn  7010  dmoprabss  7071  mpondm0  7204  elmpocl  7205  exse2  7436  fabexg  7453  frxp  7624  tposssxp  7698  dftpos4  7713  wfrdmss  7764  smores  7792  smores2  7794  iordsmo  7797  swoer  8118  swoord1  8119  swoord2  8120  ecss  8134  ecopovsym  8198  ecopovtrn  8199  ecopover  8200  sbthlem7  8428  nnfi  8505  imafi  8611  elfiun  8688  marypha1lem  8691  marypha2lem1  8693  hartogslem1  8800  wdomima2g  8844  inf3lem1  8884  tc2  8977  tz9.12lem1  9009  rankuni  9085  rankuniss  9088  rankmapu  9100  hta  9119  r0weon  9231  infxpenlem  9232  ackbij1lem9  9447  ackbij1lem10  9448  ackbij1b  9458  sdom2en01  9521  fin23lem26  9544  fin56  9612  fin1a2lem9  9627  axdc3lem  9669  axdc3lem2  9670  axcclem  9676  imadomg  9753  iundom2g  9759  smobeth  9805  canth4  9866  gruina  10037  grur1a  10038  pinn  10097  niex  10100  ltsopi  10107  ltrelpi  10108  dmaddpi  10109  dmmulpi  10110  enqex  10141  ltrelnq  10145  nqerf  10149  nqerrel  10151  dmrecnq  10187  lterpq  10189  ltrelpr  10217  enrex  10286  ltrelsr  10287  dmaddsr  10304  dmmulsr  10305  ltrelre  10353  axaddf  10364  axmulf  10365  ltrelxr  10501  lerelxr  10503  nn0ssre  11710  nn0sscn  11711  nn0ssz  11815  uzsupss  12153  rpnnen1lem1  12191  rpnnen1lem3  12192  rpnnen1lem5  12194  rpreOLD  12212  fz1ssfz0  12818  uzsup  13045  fzfi  13154  swrd00  13806  sqrlem3  14464  cau3  14575  caubnd  14578  limsupgre  14698  rlimpm  14717  rlimclim  14763  isercolllem1  14881  isercolllem2  14882  isercoll  14884  caurcvg  14893  caucvg  14895  iseraltlem2  14899  iseraltlem3  14900  zsum  14934  fsumcvg3  14945  climfsum  15034  ackbijnn  15042  divcnvshft  15069  infcvgaux1i  15071  clim2prod  15103  ntrivcvg  15112  ntrivcvgfvn0  15114  ntrivcvgtail  15115  ntrivcvgmullem  15116  ntrivcvgmul  15117  zprod  15150  dvdszrcl  15471  4sqlem1  16139  4sqlem19  16154  ramub1lem2  16218  structcnvcnv  16352  fvsetsid  16370  strleun  16446  gicer  18200  symgbasfi  18288  mvdco  18347  symgsssg  18369  efglem  18613  efgtf  18619  efgtlen  18623  efginvrel2  18624  efginvrel1  18625  efgsfo  18637  efgredlemg  18640  efgredleme  18641  efgredlemd  18642  efgredlemc  18643  efgredlem  18645  efgredlemOLD  18646  efgred  18647  efgrelexlemb  18649  efgcpbllemb  18654  frgpinv  18663  frgpuplem  18671  frgpupf  18672  frgpup1  18674  frgpnabllem2  18763  gsumval3lem1  18792  gsumval3lem2  18793  gsumval3  18794  lbsextlem3  19667  ply1bascl  20090  znf1o  20416  zntoslem  20421  pjpm  20570  dmtopon  21251  ordtbas  21520  leordtval2  21540  lecldbas  21547  lmfval  21560  lmbrf  21588  cnconst2  21611  conncompcld  21762  hauspwdom  21829  txuni2  21893  xkouni  21927  xkoccn  21947  txkgen  21980  qtoptop2  22027  kqdisj  22060  hmphtop  22106  hmpher  22112  uzrest  22225  uzfbas  22226  lmflf  22333  tgpconncompeqg  22439  tgpconncomp  22440  ustn0  22548  xmeter  22762  isngp2  22925  xrtgioo  23133  iccntr  23148  xmetdcn  23165  metdcn  23167  metdscn2  23184  icchmeo  23264  cnheiborlem  23277  lmmbrf  23584  iscau4  23601  iscauf  23602  caucfil  23605  lmclimf  23626  volf  23849  uniioombllem3  23905  uniioombllem4  23906  uniioombllem5  23907  volcn  23926  mbfimaopnlem  23975  mbflimsup  23986  i1f1  24010  itg2lcl  24047  itgioo  24135  itgsplitioo  24157  limcflflem  24197  limcflf  24198  limcresi  24202  lhop  24332  dvfsumlem1  24342  dvfsumlem2  24343  dvfsumlem3  24344  dvfsumlem4  24345  dvfsumrlimge0  24346  dvfsumrlim  24347  dvfsumrlim2  24348  dvfsum2  24350  vieta1lem1  24618  vieta1lem2  24619  psercnlem2  24731  psercnlem1  24732  psercn  24733  pserdvlem1  24734  pserdvlem2  24735  pserdv  24736  pserdv2  24737  logcnlem5  24946  dvlog  24951  dvlog2lem  24952  dvlog2  24953  dvcncxp1  25041  dvcnsqrt  25042  cxpcn3lem  25045  cxpcn3  25046  sqrtcn  25048  1cubr  25137  atansssdm  25228  jensen  25284  musum  25486  ppiub  25498  lgsquadlem1  25674  lgsquadlem2  25675  lgsquadlem3  25676  2sqlem7  25718  axtgcgrrflx  25966  axtgcgrid  25967  axtgsegcon  25968  axtg5seg  25969  axtgbtwnid  25970  axtgpasch  25971  axtgcont1  25972  tglng  26050  disjxwwlkn  27433  disjxwwlknOLD  27434  frgrwopreg2  27869  phnv  28384  htthlem  28489  hlimadd  28765  hlimcaui  28808  hhsscms  28851  occllem  28877  shjshsi  29066  3oalem4  29239  pjfi  29278  dmadjss  29461  nlelshi  29634  nlelchi  29635  hmopidmchi  29725  shatomistici  29935  difxp1ss  30073  difxp2ss  30074  fcoinver  30139  opabssi  30146  mptctf  30230  fcobijfs  30236  cyc3genpm  30498  psgnfzto1stlem  30724  cnre2csqima  30831  raddcn  30849  rrhre  30939  esumsnf  31000  sxbrsiga  31226  omssubadd  31236  carsggect  31254  sitmcl  31287  oddpwdc  31290  eulerpartlem1  31303  eulerpartlemt  31307  eulerpartgbij  31308  eulerpartlemmf  31311  eulerpartlemgh  31314  sseqf  31329  ballotlemfmpn  31431  ballotth  31474  signswch  31510  ftc2re  31550  fdvposlt  31551  fdvposle  31553  bnj1146  31744  bnj1292  31768  bnj1293  31769  bnj1145  31943  bnj1177  31956  subfacp1lem3  32047  subfacp1lem5  32049  erdszelem2  32057  kur14lem3  32073  kur14lem6  32076  kur14lem7  32077  kur14lem9  32079  cvmlift2lem12  32179  mpstssv  32339  mstapst  32347  mppspstlem  32371  mppspst  32374  mthmsta  32378  mthmpps  32382  mclsppslem  32383  dfpo2  32544  nosupbnd1lem1  32762  nosupbnd2  32770  scutf  32827  txpss3v  32893  pprodss4v  32899  relsset  32903  fixssdm  32921  fixssrn  32922  limitssson  32926  funpartss  32959  colinearex  33075  fneer  33255  neibastop1  33261  neibastop2lem  33262  filnetlem2  33281  filnetlem3  33282  knoppcnlem10  33394  bj-tagss  33843  bj-fvsnun2  34040  bj-cmnssmnd  34052  bj-ablssgrp  34054  bj-ablsscmn  34056  bj-vecssmod  34059  icoreresf  34108  icoreunrn  34115  poimirlem29  34395  poimirlem30  34396  poimirlem31  34397  poimir  34399  broucube  34400  dvasin  34452  dvacos  34453  areacirc  34461  caures  34510  bnd2lem  34544  ismtyres  34561  flddivrng  34752  xrnss3v  35102  refrelsredund2  35346  toycom  35587  dihglblem2N  37908  lcdvbase  38207  mapdunirnN  38264  prjspreln0  38700  prjspvs  38701  prjspeclsp  38703  0prjspnrel  38710  dffltz  38712  eldiophb  38783  monotuz  38968  pwssplit4  39119  pwfi2f1o  39126  arearect  39252  fvnonrel  39353  rclexi  39372  rtrclex  39374  trclexi  39377  rtrclexi  39378  clcnvlem  39380  cnvrcl0  39382  cnvtrcl0  39383  dfrtrcl5  39386  dfrcl2  39416  comptiunov2i  39448  corclrcl  39449  trclrelexplem  39453  relexpaddss  39460  cotrcltrcl  39467  corcltrcl  39481  cotrclrcl  39484  frege131d  39506  rp-imass  39514  0he  39525  grumnudlem  40030  uzmptshftfval  40128  binomcxplemdvbinom  40135  binomcxplemdvsum  40137  binomcxplemnotnn0  40138  rabexgf  40734  uzct  40778  disjf1o  40907  dmresss  40958  dmmptssf  40960  mptssid  40969  uzfissfz  41053  ssuzfz  41076  uzssre2  41141  uzublem  41165  uzssz2  41193  uzsscn2  41215  sumnnodd  41372  climconstmpt  41400  fnlimfvre  41416  fnlimabslt  41421  limsupvaluz  41450  limsupubuzlem  41454  limsupubuz  41455  limsupequzmpt2  41460  limsupmnfuzlem  41468  limsupre3uzlem  41477  liminfequzmpt2  41533  ibliooicc  41716  stoweidlem44  41790  stoweidlem50  41796  stoweidlem51  41797  stoweidlem52  41798  stoweidlem57  41803  stoweidlem59  41805  fourierdlem16  41869  fourierdlem19  41872  fourierdlem21  41874  fourierdlem22  41875  fourierdlem42  41895  fourierdlem83  41935  fouriersw  41977  salexct  42078  salexct3  42086  salgencntex  42087  salgensscntex  42088  sge0less  42135  sge0fodjrnlem  42159  sge0isum  42170  ovnsslelem  42303  ovnlerp  42305  ovn0lem  42308  hoidmv1lelem1  42334  hoidmv1lelem3  42336  hoidmvlelem1  42338  hoidmvlelem2  42339  hoidmvlelem3  42340  hoidmvlelem4  42341  ovnhoilem1  42344  ovnhoilem2  42345  opnvonmbllem2  42376  ovolval4lem1  42392  ovolval5lem3  42397  pimdecfgtioc  42454  pimincfltioc  42455  pimdecfgtioo  42456  pimincfltioo  42457  incsmflem  42479  decsmflem  42503  smflimlem2  42509  smflimlem3  42510  smflim  42514  smfrec  42525  smfmullem4  42530  smfdiv  42533  smfsuplem1  42546  smfsuplem3  42548  smfsupxr  42551  smfliminflem  42565  oddibas  43478  2zlidl  43599  2zrngbas  43601  2zrng0  43603  fldc  43748  fldhmsubc  43749  fldcALTV  43766  fldhmsubcALTV  43767  setrec2lem1  44193