Theorem eqsstri 3996

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

Syntax hints:   = wceq 1540   ⊆ wss 3917

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2722  df-ss 3934

This theorem is referenced by:  eqsstrri  3997  3sstr4i  4001  ssrab3  4048  rabssab  4051  ifssun  4509  opabss  5174  brab2a  5735  relopabiALT  5789  dmopabss  5885  rnopabss  5922  resss  5975  relres  5979  rnin  6122  rnxpss  6148  cnvcnvss  6170  resdmss  6211  resssxp  6246  dfpo2  6272  predss  6285  fnres  6648  f0  6744  nfvres  6902  fvopab4ndm  7001  ffvresb  7100  mptexgf  7199  funiunfv  7225  isoini2  7317  ovssunirn  7426  dmoprabss  7496  mpondm0  7632  elmpocl  7633  exse2  7896  fabexgOLD  7918  frxp  8108  tposssxp  8212  dftpos4  8227  smores  8324  smores2  8326  iordsmo  8329  swoer  8705  swoord1  8706  swoord2  8707  ecss  8725  ecopovsym  8795  ecopovtrn  8796  ecopover  8797  f1setex  8833  sbthlem7  9063  imafi  9271  elfiun  9388  marypha1lem  9391  marypha2lem1  9393  hartogslem1  9502  wdomima2g  9546  inf3lem1  9588  dmttrcl  9681  rnttrcl  9682  tc2  9702  frmin  9709  frrlem16  9718  frr1  9719  tz9.12lem1  9747  rankuni  9823  rankuniss  9826  rankmapu  9838  hta  9857  r0weon  9972  infxpenlem  9973  ackbij1lem9  10187  ackbij1lem10  10188  ackbij1b  10198  sdom2en01  10262  fin23lem26  10285  fin56  10353  fin1a2lem9  10368  axdc3lem  10410  axdc3lem2  10411  axcclem  10417  imadomg  10494  iundom2g  10500  smobeth  10546  canth4  10607  gruina  10778  grur1a  10779  pinn  10838  niex  10841  ltsopi  10848  ltrelpi  10849  dmaddpi  10850  dmmulpi  10851  enqex  10882  ltrelnq  10886  nqerf  10890  nqerrel  10892  dmrecnq  10928  lterpq  10930  ltrelpr  10958  enrex  11027  ltrelsr  11028  dmaddsr  11045  dmmulsr  11046  ltrelre  11094  axaddf  11105  axmulf  11106  ltrelxr  11242  lerelxr  11244  nn0ssre  12453  nn0sscn  12454  nn0ssz  12559  uzsupss  12906  rpnnen1lem1  12944  rpnnen1lem3  12945  rpnnen1lem5  12947  fz1ssfz0  13591  uzsup  13832  fzfi  13944  swrd00  14616  01sqrexlem3  15217  cau3  15329  caubnd  15332  limsupgre  15454  rlimpm  15473  rlimclim  15519  isercolllem1  15638  isercolllem2  15639  isercoll  15641  caurcvg  15650  caucvg  15652  iseraltlem2  15656  iseraltlem3  15657  zsum  15691  fsumcvg3  15702  climfsum  15793  ackbijnn  15801  divcnvshft  15828  infcvgaux1i  15830  clim2prod  15861  ntrivcvg  15870  ntrivcvgfvn0  15872  ntrivcvgtail  15873  ntrivcvgmullem  15874  ntrivcvgmul  15875  zprod  15910  dvdszrcl  16234  4sqlem1  16926  4sqlem19  16941  ramub1lem2  17005  structcnvcnv  17130  strleun  17134  fvsetsid  17145  smndex1sgrp  18842  gicer  19216  cntzsgrpcl  19273  symgbasfi  19316  mvdco  19382  symgsssg  19404  efglem  19653  efgtf  19659  efgtlen  19663  efginvrel2  19664  efginvrel1  19665  efgsfo  19676  efgredlemg  19679  efgredleme  19680  efgredlemd  19681  efgredlemc  19682  efgredlem  19684  efgred  19685  efgrelexlemb  19687  efgcpbllemb  19692  frgpinv  19701  frgpuplem  19709  frgpupf  19710  frgpup1  19712  frgpnabllem2  19811  gsumval3lem1  19842  gsumval3lem2  19843  gsumval3  19844  fldc  20700  fldhmsubc  20701  lbsextlem3  21077  pzriprnglem10  21407  znf1o  21468  zntoslem  21473  pjpm  21624  mhp0cl  22040  ply1bascl  22095  dmtopon  22817  ordtbas  23086  leordtval2  23106  lecldbas  23113  lmfval  23126  lmbrf  23154  cnconst2  23177  conncompcld  23328  hauspwdom  23395  txuni2  23459  xkouni  23493  xkoccn  23513  txkgen  23546  qtoptop2  23593  kqdisj  23626  hmphtop  23672  hmpher  23678  uzrest  23791  uzfbas  23792  lmflf  23899  tgpconncompeqg  24006  tgpconncomp  24007  ustn0  24115  xmeter  24328  isngp2  24492  xrtgioo  24702  iccntr  24717  xmetdcn  24734  metdcn  24736  metdscn2  24753  icchmeoOLD  24846  cnheiborlem  24860  reparphti  24903  lmmbrf  25169  iscau4  25186  iscauf  25187  caucfil  25190  lmclimf  25211  volf  25437  uniioombllem3  25493  uniioombllem4  25494  uniioombllem5  25495  volcn  25514  mbfimaopnlem  25563  mbflimsup  25574  i1f1  25598  itg2lcl  25635  itgioo  25724  itgsplitioo  25746  limcflflem  25788  limcflf  25789  limcresi  25793  lhop  25928  dvfsumlem1  25939  dvfsumlem2  25940  dvfsumlem2OLD  25941  dvfsumlem3  25942  dvfsumlem4  25943  dvfsumrlimge0  25944  dvfsumrlim  25945  dvfsumrlim2  25946  dvfsum2  25948  vieta1lem1  26225  vieta1lem2  26226  psercnlem2  26341  psercnlem1  26342  psercn  26343  pserdvlem1  26344  pserdvlem2  26345  pserdv  26346  pserdv2  26347  logcnlem5  26562  dvlog  26567  dvlog2lem  26568  dvlog2  26569  dvcncxp1  26659  dvcnsqrt  26660  cxpcn3lem  26664  cxpcn3  26665  sqrtcn  26667  1cubr  26759  atansssdm  26850  jensen  26906  musum  27108  ppiub  27122  lgsquadlem1  27298  lgsquadlem2  27299  lgsquadlem3  27300  2sqlem7  27342  nosupbnd1lem1  27627  nosupbnd2  27635  noinfbnd1lem1  27642  scutf  27731  leftssold  27797  rightssold  27798  mulsproplem12  28037  mulsproplem13  28038  mulsproplem14  28039  precsexlem8  28123  onssno  28162  nnssn0s  28221  dfnns2  28268  axtgcgrrflx  28396  axtgcgrid  28397  axtgsegcon  28398  axtg5seg  28399  axtgbtwnid  28400  axtgpasch  28401  axtgcont1  28402  tglng  28480  disjxwwlkn  29850  frgrwopreg2  30255  phnv  30750  htthlem  30853  hlimadd  31129  hlimcaui  31172  hhsscms  31214  occllem  31239  shjshsi  31428  3oalem4  31601  pjfi  31640  dmadjss  31823  nlelshi  31996  nlelchi  31997  hmopidmchi  32087  shatomistici  32297  difxp1ss  32458  difxp2ss  32459  fcoinver  32540  opabssi  32548  mptctf  32648  ccatws1f1o  32880  gsumpart  33004  pmtrcnel2  33054  psgnfzto1stlem  33064  cycpmrn  33107  cyc3genpm  33116  unitprodclb  33367  lsmsnorb  33369  ply1degltel  33567  ply1degleel  33568  ply1degltlss  33569  constrsscn  33737  cnre2csqima  33908  raddcn  33926  zrhcntr  33976  rrhre  34018  esumsnf  34061  sxbrsiga  34288  omssubadd  34298  carsggect  34316  sitmcl  34349  oddpwdc  34352  eulerpartlem1  34365  eulerpartlemt  34369  eulerpartgbij  34370  eulerpartlemmf  34373  eulerpartlemgh  34376  sseqf  34390  ballotlemfmpn  34493  ballotth  34536  signswch  34559  ftc2re  34596  fdvposlt  34597  fdvposle  34599  bnj1146  34788  bnj1292  34812  bnj1293  34813  bnj1145  34990  bnj1177  35003  erdszelem2  35186  kur14lem3  35202  kur14lem6  35205  kur14lem7  35206  kur14lem9  35208  cvmlift2lem12  35308  mpstssv  35533  mstapst  35541  mppspstlem  35565  mppspst  35568  mthmsta  35572  mthmpps  35576  mclsppslem  35577  txpss3v  35873  pprodss4v  35879  relsset  35883  fixssdm  35901  fixssrn  35902  limitssson  35906  funpartss  35939  colinearex  36055  fneer  36348  neibastop1  36354  neibastop2lem  36355  filnetlem2  36374  filnetlem3  36375  knoppcnlem10  36497  bj-tagss  36975  bj-imdirco  37185  bj-fvsnun2  37251  bj-ablssgrp  37271  bj-ablsscmn  37273  bj-vecssmod  37276  bj-fldssdrng  37283  icoreresf  37347  icoreunrn  37354  poimirlem29  37650  poimirlem30  37651  poimirlem31  37652  poimir  37654  broucube  37655  dvasin  37705  dvacos  37706  areacirc  37714  caures  37761  bnd2lem  37792  ismtyres  37809  flddivrng  38000  xrnss3v  38361  refrelsredund2  38631  toycom  38973  dihglblem2N  41295  lcdvbase  41594  mapdunirnN  41651  aks6d1c1p1rcl  42103  redvmptabs  42355  readvrec  42357  prjspreln0  42604  prjspvs  42605  prjspeclsp  42607  0prjspnrel  42622  dffltz  42629  eldiophb  42752  monotuz  42937  pwssplit4  43085  pwfi2f1o  43092  arearect  43211  cantnfresb  43320  omabs2  43328  fvnonrel  43593  rclexi  43611  rtrclex  43613  trclexi  43616  rtrclexi  43617  clcnvlem  43619  cnvrcl0  43621  cnvtrcl0  43622  dfrtrcl5  43625  dfrcl2  43670  comptiunov2i  43702  corclrcl  43703  trclrelexplem  43707  relexpaddss  43714  cotrcltrcl  43721  corcltrcl  43735  cotrclrcl  43738  frege131d  43760  0he  43778  grumnudlem  44281  uzmptshftfval  44342  binomcxplemdvbinom  44349  binomcxplemdvsum  44351  binomcxplemnotnn0  44352  modelaxreplem2  44976  rabexgf  45025  uzct  45064  disjf1o  45192  dmmptssf  45233  mptssid  45242  uzfissfz  45329  ssuzfz  45352  uzssre2  45410  uzublem  45433  uzssz2  45459  uzsscn2  45480  sumnnodd  45635  climconstmpt  45663  fnlimfvre  45679  fnlimabslt  45684  limsupvaluz  45713  limsupubuzlem  45717  limsupubuz  45718  limsupequzmpt2  45723  limsupmnfuzlem  45731  limsupre3uzlem  45740  liminfequzmpt2  45796  ibliooicc  45976  stoweidlem44  46049  stoweidlem50  46055  stoweidlem51  46056  stoweidlem52  46057  stoweidlem57  46062  stoweidlem59  46064  fourierdlem16  46128  fourierdlem19  46131  fourierdlem21  46133  fourierdlem22  46134  fourierdlem42  46154  fourierdlem83  46194  fouriersw  46236  salexct  46339  salexct3  46347  salgencntex  46348  salgensscntex  46349  sge0less  46397  sge0fodjrnlem  46421  sge0isum  46432  ovnlerp  46567  ovn0lem  46570  hoidmv1lelem1  46596  hoidmv1lelem3  46598  hoidmvlelem1  46600  hoidmvlelem2  46601  hoidmvlelem3  46602  hoidmvlelem4  46603  ovnhoilem1  46606  ovnhoilem2  46607  opnvonmbllem2  46638  ovolval4lem1  46654  ovolval5lem3  46659  pimdecfgtioc  46720  pimincfltioc  46721  pimdecfgtioo  46722  pimincfltioo  46723  incsmflem  46746  decsmflem  46771  smflimlem2  46777  smflimlem3  46778  smflim  46782  smfrec  46794  smfmullem4  46799  smfdiv  46802  smfsuplem1  46816  smfsuplem3  46818  smfsupxr  46821  smfliminflem  46835  cfsetssfset  47061  fcoreslem2  47069  fcores  47072  gricrel  47923  clnbgrisubgrgrim  47936  isubgr3stgrlem6  47974  isubgr3stgrlem7  47975  isubgr3stgrlem8  47976  isubgr3stgr  47978  grlimgrtrilem2  47998  grlicrel  48002  oddibas  48165  2zlidl  48232  2zrngbas  48234  2zrng0  48236  fldcALTV  48324  fldhmsubcALTV  48325  dmtposss  48868  tposres3  48873  ipolub0  48984  imaidfu  49103