Theorem eqsstri 3982

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

Syntax hints:   = wceq 1542   ⊆ wss 3903

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729  df-ss 3920

This theorem is referenced by:  eqsstrri  3983  3sstr4i  3987  ssrab3  4036  rabssab  4039  ifssun  4499  opabss  5164  brab2a  5727  relopabiALT  5782  dmopabss  5877  rnopabss  5914  resss  5970  relres  5974  rnin  6114  rnxpss  6140  cnvcnvss  6162  resdmss  6203  resssxp  6238  dfpo2  6264  predss  6277  fnres  6629  f0  6725  nfvres  6882  fvopab4ndm  6982  ffvresb  7082  mptexgf  7180  funiunfv  7206  isoini2  7297  ovssunirn  7406  dmoprabss  7474  mpondm0  7610  elmpocl  7611  exse2  7871  fabexgOLD  7893  frxp  8080  tposssxp  8184  dftpos4  8199  smores  8296  smores2  8298  iordsmo  8301  swoer  8679  swoord1  8680  swoord2  8681  ecss  8699  ecopovsym  8770  ecopovtrn  8771  ecopover  8772  f1setex  8808  sbthlem7  9035  imafi  9229  elfiun  9347  marypha1lem  9350  marypha2lem1  9352  hartogslem1  9461  wdomima2g  9505  inf3lem1  9551  dmttrcl  9644  rnttrcl  9645  tc2  9663  frmin  9675  frrlem16  9684  frr1  9685  tz9.12lem1  9713  rankuni  9789  rankuniss  9792  rankmapu  9804  hta  9823  r0weon  9936  infxpenlem  9937  ackbij1lem9  10151  ackbij1lem10  10152  ackbij1b  10162  sdom2en01  10226  fin23lem26  10249  fin56  10317  fin1a2lem9  10332  axdc3lem  10374  axdc3lem2  10375  axcclem  10381  imadomg  10458  iundom2g  10464  smobeth  10511  canth4  10572  gruina  10743  grur1a  10744  pinn  10803  niex  10806  ltsopi  10813  ltrelpi  10814  dmaddpi  10815  dmmulpi  10816  enqex  10847  ltrelnq  10851  nqerf  10855  nqerrel  10857  dmrecnq  10893  lterpq  10895  ltrelpr  10923  enrex  10992  ltrelsr  10993  dmaddsr  11010  dmmulsr  11011  ltrelre  11059  axaddf  11070  axmulf  11071  ltrelxr  11207  lerelxr  11209  nn0ssre  12419  nn0sscn  12420  nn0ssz  12525  uzsupss  12867  rpnnen1lem1  12905  rpnnen1lem3  12906  rpnnen1lem5  12908  fz1ssfz0  13553  uzsup  13797  fzfi  13909  swrd00  14582  01sqrexlem3  15181  cau3  15293  caubnd  15296  limsupgre  15418  rlimpm  15437  rlimclim  15483  isercolllem1  15602  isercolllem2  15603  isercoll  15605  caurcvg  15614  caucvg  15616  iseraltlem2  15620  iseraltlem3  15621  zsum  15655  fsumcvg3  15666  climfsum  15757  ackbijnn  15765  divcnvshft  15792  infcvgaux1i  15794  clim2prod  15825  ntrivcvg  15834  ntrivcvgfvn0  15836  ntrivcvgtail  15837  ntrivcvgmullem  15838  ntrivcvgmul  15839  zprod  15874  dvdszrcl  16198  4sqlem1  16890  4sqlem19  16905  ramub1lem2  16969  structcnvcnv  17094  strleun  17098  fvsetsid  17109  smndex1sgrp  18850  gicer  19223  cntzsgrpcl  19280  symgbasfi  19325  mvdco  19391  symgsssg  19413  efglem  19662  efgtf  19668  efgtlen  19672  efginvrel2  19673  efginvrel1  19674  efgsfo  19685  efgredlemg  19688  efgredleme  19689  efgredlemd  19690  efgredlemc  19691  efgredlem  19693  efgred  19694  efgrelexlemb  19696  efgcpbllemb  19701  frgpinv  19710  frgpuplem  19718  frgpupf  19719  frgpup1  19721  frgpnabllem2  19820  gsumval3lem1  19851  gsumval3lem2  19852  gsumval3  19853  fldc  20734  fldhmsubc  20735  lbsextlem3  21132  pzriprnglem10  21462  znf1o  21523  zntoslem  21528  pjpm  21680  mhp0cl  22106  ply1bascl  22161  dmtopon  22884  ordtbas  23153  leordtval2  23173  lecldbas  23180  lmfval  23193  lmbrf  23221  cnconst2  23244  conncompcld  23395  hauspwdom  23462  txuni2  23526  xkouni  23560  xkoccn  23580  txkgen  23613  qtoptop2  23660  kqdisj  23693  hmphtop  23739  hmpher  23745  uzrest  23858  uzfbas  23859  lmflf  23966  tgpconncompeqg  24073  tgpconncomp  24074  ustn0  24182  xmeter  24394  isngp2  24558  xrtgioo  24768  iccntr  24783  xmetdcn  24800  metdcn  24802  metdscn2  24819  icchmeoOLD  24912  cnheiborlem  24926  reparphti  24969  lmmbrf  25235  iscau4  25252  iscauf  25253  caucfil  25256  lmclimf  25277  volf  25503  uniioombllem3  25559  uniioombllem4  25560  uniioombllem5  25561  volcn  25580  mbfimaopnlem  25629  mbflimsup  25640  i1f1  25664  itg2lcl  25701  itgioo  25790  itgsplitioo  25812  limcflflem  25854  limcflf  25855  limcresi  25859  lhop  25994  dvfsumlem1  26005  dvfsumlem2  26006  dvfsumlem2OLD  26007  dvfsumlem3  26008  dvfsumlem4  26009  dvfsumrlimge0  26010  dvfsumrlim  26011  dvfsumrlim2  26012  dvfsum2  26014  vieta1lem1  26291  vieta1lem2  26292  psercnlem2  26407  psercnlem1  26408  psercn  26409  pserdvlem1  26410  pserdvlem2  26411  pserdv  26412  pserdv2  26413  logcnlem5  26628  dvlog  26633  dvlog2lem  26634  dvlog2  26635  dvcncxp1  26725  dvcnsqrt  26726  cxpcn3lem  26730  cxpcn3  26731  sqrtcn  26733  1cubr  26825  atansssdm  26916  jensen  26972  musum  27174  ppiub  27188  lgsquadlem1  27364  lgsquadlem2  27365  lgsquadlem3  27366  2sqlem7  27408  nosupbnd1lem1  27693  nosupbnd2  27701  noinfbnd1lem1  27708  cutsf  27805  leftssold  27884  rightssold  27885  mulsproplem12  28140  mulsproplem13  28141  mulsproplem14  28142  precsexlem8  28227  onssno  28267  nnssn0s  28334  dfnns2  28385  bdaypw2n0bndlem  28476  axtgcgrrflx  28552  axtgcgrid  28553  axtgsegcon  28554  axtg5seg  28555  axtgbtwnid  28556  axtgpasch  28557  axtgcont1  28558  tglng  28636  disjxwwlkn  30004  frgrwopreg2  30412  phnv  30908  htthlem  31011  hlimadd  31287  hlimcaui  31330  hhsscms  31372  occllem  31397  shjshsi  31586  3oalem4  31759  pjfi  31798  dmadjss  31981  nlelshi  32154  nlelchi  32155  hmopidmchi  32245  shatomistici  32455  difxp1ss  32615  difxp2ss  32616  fcoinver  32697  opabssi  32709  mptctf  32812  ccatws1f1o  33050  gsumpart  33163  pmtrcnel2  33190  psgnfzto1stlem  33200  cycpmrn  33243  cyc3genpm  33252  unitprodclb  33488  lsmsnorb  33490  ply1degltel  33693  ply1degleel  33694  ply1degltlss  33695  evlextv  33725  vietalem  33762  constrsscn  33924  cnre2csqima  34095  raddcn  34113  zrhcntr  34163  rrhre  34205  esumsnf  34248  sxbrsiga  34474  omssubadd  34484  carsggect  34502  sitmcl  34535  oddpwdc  34538  eulerpartlem1  34551  eulerpartlemt  34555  eulerpartgbij  34556  eulerpartlemmf  34559  eulerpartlemgh  34562  sseqf  34576  ballotlemfmpn  34679  ballotth  34722  signswch  34745  ftc2re  34782  fdvposlt  34783  fdvposle  34785  bnj1146  34973  bnj1292  34997  bnj1293  34998  bnj1145  35175  bnj1177  35188  fineqvnttrclse  35308  tz9.1regs  35318  erdszelem2  35414  kur14lem3  35430  kur14lem6  35433  kur14lem7  35434  kur14lem9  35436  cvmlift2lem12  35536  mpstssv  35761  mstapst  35769  mppspstlem  35793  mppspst  35796  mthmsta  35800  mthmpps  35804  mclsppslem  35805  txpss3v  36098  pprodss4v  36104  relsset  36108  fixssdm  36126  fixssrn  36127  limitssson  36131  funpartss  36166  colinearex  36282  fneer  36575  neibastop1  36581  neibastop2lem  36582  filnetlem2  36601  filnetlem3  36602  knoppcnlem10  36730  bj-tagss  37255  bj-imdirco  37472  bj-fvsnun2  37538  bj-ablssgrp  37558  bj-ablsscmn  37560  bj-vecssmod  37563  bj-fldssdrng  37570  icoreresf  37634  icoreunrn  37641  poimirlem29  37929  poimirlem30  37930  poimirlem31  37931  poimir  37933  broucube  37934  dvasin  37984  dvacos  37985  areacirc  37993  caures  38040  bnd2lem  38071  ismtyres  38088  flddivrng  38279  xrnss3v  38661  refrelsredund2  38997  toycom  39378  dihglblem2N  41699  lcdvbase  41998  mapdunirnN  42055  aks6d1c1p1rcl  42507  redvmptabs  42759  readvrec  42761  prjspreln0  42996  prjspvs  42997  prjspeclsp  42999  0prjspnrel  43014  dffltz  43021  eldiophb  43143  monotuz  43327  pwssplit4  43475  pwfi2f1o  43482  arearect  43601  cantnfresb  43710  omabs2  43718  fvnonrel  43982  rclexi  44000  rtrclex  44002  trclexi  44005  rtrclexi  44006  clcnvlem  44008  cnvrcl0  44010  cnvtrcl0  44011  dfrtrcl5  44014  dfrcl2  44059  comptiunov2i  44091  corclrcl  44092  trclrelexplem  44096  relexpaddss  44103  cotrcltrcl  44110  corcltrcl  44124  cotrclrcl  44127  frege131d  44149  0he  44167  grumnudlem  44670  uzmptshftfval  44731  binomcxplemdvbinom  44738  binomcxplemdvsum  44740  binomcxplemnotnn0  44741  modelaxreplem2  45364  rabexgf  45413  uzct  45452  disjf1o  45579  dmmptssf  45619  mptssid  45628  uzfissfz  45714  ssuzfz  45737  uzssre2  45794  uzublem  45817  uzssz2  45843  uzsscn2  45864  sumnnodd  46019  climconstmpt  46045  fnlimfvre  46061  fnlimabslt  46066  limsupvaluz  46095  limsupubuzlem  46099  limsupubuz  46100  limsupequzmpt2  46105  limsupmnfuzlem  46113  limsupre3uzlem  46122  liminfequzmpt2  46178  ibliooicc  46358  stoweidlem44  46431  stoweidlem50  46437  stoweidlem51  46438  stoweidlem52  46439  stoweidlem57  46444  stoweidlem59  46446  fourierdlem16  46510  fourierdlem19  46513  fourierdlem21  46515  fourierdlem22  46516  fourierdlem42  46536  fourierdlem83  46576  fouriersw  46618  salexct  46721  salexct3  46729  salgencntex  46730  salgensscntex  46731  sge0less  46779  sge0fodjrnlem  46803  sge0isum  46814  ovnlerp  46949  ovn0lem  46952  hoidmv1lelem1  46978  hoidmv1lelem3  46980  hoidmvlelem1  46982  hoidmvlelem2  46983  hoidmvlelem3  46984  hoidmvlelem4  46985  ovnhoilem1  46988  ovnhoilem2  46989  opnvonmbllem2  47020  ovolval4lem1  47036  ovolval5lem3  47041  pimdecfgtioc  47102  pimincfltioc  47103  pimdecfgtioo  47104  pimincfltioo  47105  incsmflem  47128  decsmflem  47153  smflimlem2  47159  smflimlem3  47160  smflim  47164  smfrec  47176  smfmullem4  47181  smfdiv  47184  smfsuplem1  47198  smfsuplem3  47200  smfsupxr  47203  smfliminflem  47217  cfsetssfset  47445  fcoreslem2  47453  fcores  47456  gricrel  48308  clnbgrisubgrgrim  48321  isubgr3stgrlem6  48360  isubgr3stgrlem7  48361  isubgr3stgrlem8  48362  isubgr3stgr  48364  grlimgrtrilem2  48391  grlicrel  48395  oddibas  48562  2zlidl  48629  2zrngbas  48631  2zrng0  48633  fldcALTV  48721  fldhmsubcALTV  48722  dmtposss  49264  tposres3  49269  ipolub0  49380  imaidfu  49498