Theorem eqsstri 4005

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

Syntax hints:   = wceq 1540   ⊆ wss 3926

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 2007  ax-9 2118  ax-ext 2707

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

This theorem is referenced by:  eqsstrri  4006  3sstr4i  4010  ssrab3  4057  rabssab  4060  ifssun  4518  opabss  5183  brab2a  5748  relopabiALT  5802  dmopabss  5898  rnopabss  5935  resss  5988  relres  5992  rnin  6135  rnxpss  6161  cnvcnvss  6183  resdmss  6224  resssxp  6259  dfpo2  6285  predss  6298  fnres  6665  f0  6759  nfvres  6917  fvopab4ndm  7016  ffvresb  7115  mptexgf  7214  funiunfv  7240  isoini2  7332  ovssunirn  7441  dmoprabss  7511  mpondm0  7647  elmpocl  7648  exse2  7913  fabexgOLD  7935  frxp  8125  tposssxp  8229  dftpos4  8244  wfrdmssOLD  8329  smores  8366  smores2  8368  iordsmo  8371  swoer  8750  swoord1  8751  swoord2  8752  ecss  8767  ecopovsym  8833  ecopovtrn  8834  ecopover  8835  f1setex  8871  sbthlem7  9103  imafi  9325  elfiun  9442  marypha1lem  9445  marypha2lem1  9447  hartogslem1  9556  wdomima2g  9600  inf3lem1  9642  dmttrcl  9735  rnttrcl  9736  tc2  9756  frmin  9763  frrlem16  9772  frr1  9773  tz9.12lem1  9801  rankuni  9877  rankuniss  9880  rankmapu  9892  hta  9911  r0weon  10026  infxpenlem  10027  ackbij1lem9  10241  ackbij1lem10  10242  ackbij1b  10252  sdom2en01  10316  fin23lem26  10339  fin56  10407  fin1a2lem9  10422  axdc3lem  10464  axdc3lem2  10465  axcclem  10471  imadomg  10548  iundom2g  10554  smobeth  10600  canth4  10661  gruina  10832  grur1a  10833  pinn  10892  niex  10895  ltsopi  10902  ltrelpi  10903  dmaddpi  10904  dmmulpi  10905  enqex  10936  ltrelnq  10940  nqerf  10944  nqerrel  10946  dmrecnq  10982  lterpq  10984  ltrelpr  11012  enrex  11081  ltrelsr  11082  dmaddsr  11099  dmmulsr  11100  ltrelre  11148  axaddf  11159  axmulf  11160  ltrelxr  11296  lerelxr  11298  nn0ssre  12505  nn0sscn  12506  nn0ssz  12611  uzsupss  12956  rpnnen1lem1  12994  rpnnen1lem3  12995  rpnnen1lem5  12997  fz1ssfz0  13640  uzsup  13880  fzfi  13990  swrd00  14662  01sqrexlem3  15263  cau3  15374  caubnd  15377  limsupgre  15497  rlimpm  15516  rlimclim  15562  isercolllem1  15681  isercolllem2  15682  isercoll  15684  caurcvg  15693  caucvg  15695  iseraltlem2  15699  iseraltlem3  15700  zsum  15734  fsumcvg3  15745  climfsum  15836  ackbijnn  15844  divcnvshft  15871  infcvgaux1i  15873  clim2prod  15904  ntrivcvg  15913  ntrivcvgfvn0  15915  ntrivcvgtail  15916  ntrivcvgmullem  15917  ntrivcvgmul  15918  zprod  15953  dvdszrcl  16277  4sqlem1  16968  4sqlem19  16983  ramub1lem2  17047  structcnvcnv  17172  strleun  17176  fvsetsid  17187  smndex1sgrp  18886  gicer  19260  cntzsgrpcl  19317  symgbasfi  19360  mvdco  19426  symgsssg  19448  efglem  19697  efgtf  19703  efgtlen  19707  efginvrel2  19708  efginvrel1  19709  efgsfo  19720  efgredlemg  19723  efgredleme  19724  efgredlemd  19725  efgredlemc  19726  efgredlem  19728  efgred  19729  efgrelexlemb  19731  efgcpbllemb  19736  frgpinv  19745  frgpuplem  19753  frgpupf  19754  frgpup1  19756  frgpnabllem2  19855  gsumval3lem1  19886  gsumval3lem2  19887  gsumval3  19888  fldc  20744  fldhmsubc  20745  lbsextlem3  21121  pzriprnglem10  21451  znf1o  21512  zntoslem  21517  pjpm  21668  mhp0cl  22084  ply1bascl  22139  dmtopon  22861  ordtbas  23130  leordtval2  23150  lecldbas  23157  lmfval  23170  lmbrf  23198  cnconst2  23221  conncompcld  23372  hauspwdom  23439  txuni2  23503  xkouni  23537  xkoccn  23557  txkgen  23590  qtoptop2  23637  kqdisj  23670  hmphtop  23716  hmpher  23722  uzrest  23835  uzfbas  23836  lmflf  23943  tgpconncompeqg  24050  tgpconncomp  24051  ustn0  24159  xmeter  24372  isngp2  24536  xrtgioo  24746  iccntr  24761  xmetdcn  24778  metdcn  24780  metdscn2  24797  icchmeoOLD  24890  cnheiborlem  24904  reparphti  24947  lmmbrf  25214  iscau4  25231  iscauf  25232  caucfil  25235  lmclimf  25256  volf  25482  uniioombllem3  25538  uniioombllem4  25539  uniioombllem5  25540  volcn  25559  mbfimaopnlem  25608  mbflimsup  25619  i1f1  25643  itg2lcl  25680  itgioo  25769  itgsplitioo  25791  limcflflem  25833  limcflf  25834  limcresi  25838  lhop  25973  dvfsumlem1  25984  dvfsumlem2  25985  dvfsumlem2OLD  25986  dvfsumlem3  25987  dvfsumlem4  25988  dvfsumrlimge0  25989  dvfsumrlim  25990  dvfsumrlim2  25991  dvfsum2  25993  vieta1lem1  26270  vieta1lem2  26271  psercnlem2  26386  psercnlem1  26387  psercn  26388  pserdvlem1  26389  pserdvlem2  26390  pserdv  26391  pserdv2  26392  logcnlem5  26607  dvlog  26612  dvlog2lem  26613  dvlog2  26614  dvcncxp1  26704  dvcnsqrt  26705  cxpcn3lem  26709  cxpcn3  26710  sqrtcn  26712  1cubr  26804  atansssdm  26895  jensen  26951  musum  27153  ppiub  27167  lgsquadlem1  27343  lgsquadlem2  27344  lgsquadlem3  27345  2sqlem7  27387  nosupbnd1lem1  27672  nosupbnd2  27680  noinfbnd1lem1  27687  scutf  27776  leftssold  27842  rightssold  27843  mulsproplem12  28082  mulsproplem13  28083  mulsproplem14  28084  precsexlem8  28168  onssno  28207  nnssn0s  28266  dfnns2  28313  axtgcgrrflx  28441  axtgcgrid  28442  axtgsegcon  28443  axtg5seg  28444  axtgbtwnid  28445  axtgpasch  28446  axtgcont1  28447  tglng  28525  disjxwwlkn  29895  frgrwopreg2  30300  phnv  30795  htthlem  30898  hlimadd  31174  hlimcaui  31217  hhsscms  31259  occllem  31284  shjshsi  31473  3oalem4  31646  pjfi  31685  dmadjss  31868  nlelshi  32041  nlelchi  32042  hmopidmchi  32132  shatomistici  32342  difxp1ss  32503  difxp2ss  32504  fcoinver  32585  opabssi  32593  mptctf  32695  ccatws1f1o  32927  gsumpart  33051  pmtrcnel2  33101  psgnfzto1stlem  33111  cycpmrn  33154  cyc3genpm  33163  unitprodclb  33404  lsmsnorb  33406  ply1degltel  33604  ply1degleel  33605  ply1degltlss  33606  constrsscn  33774  cnre2csqima  33942  raddcn  33960  zrhcntr  34010  rrhre  34052  esumsnf  34095  sxbrsiga  34322  omssubadd  34332  carsggect  34350  sitmcl  34383  oddpwdc  34386  eulerpartlem1  34399  eulerpartlemt  34403  eulerpartgbij  34404  eulerpartlemmf  34407  eulerpartlemgh  34410  sseqf  34424  ballotlemfmpn  34527  ballotth  34570  signswch  34593  ftc2re  34630  fdvposlt  34631  fdvposle  34633  bnj1146  34822  bnj1292  34846  bnj1293  34847  bnj1145  35024  bnj1177  35037  erdszelem2  35214  kur14lem3  35230  kur14lem6  35233  kur14lem7  35234  kur14lem9  35236  cvmlift2lem12  35336  mpstssv  35561  mstapst  35569  mppspstlem  35593  mppspst  35596  mthmsta  35600  mthmpps  35604  mclsppslem  35605  txpss3v  35896  pprodss4v  35902  relsset  35906  fixssdm  35924  fixssrn  35925  limitssson  35929  funpartss  35962  colinearex  36078  fneer  36371  neibastop1  36377  neibastop2lem  36378  filnetlem2  36397  filnetlem3  36398  knoppcnlem10  36520  bj-tagss  36998  bj-imdirco  37208  bj-fvsnun2  37274  bj-ablssgrp  37294  bj-ablsscmn  37296  bj-vecssmod  37299  bj-fldssdrng  37306  icoreresf  37370  icoreunrn  37377  poimirlem29  37673  poimirlem30  37674  poimirlem31  37675  poimir  37677  broucube  37678  dvasin  37728  dvacos  37729  areacirc  37737  caures  37784  bnd2lem  37815  ismtyres  37832  flddivrng  38023  xrnss3v  38390  refrelsredund2  38651  toycom  38991  dihglblem2N  41313  lcdvbase  41612  mapdunirnN  41669  aks6d1c1p1rcl  42121  redvmptabs  42403  readvrec  42405  prjspreln0  42632  prjspvs  42633  prjspeclsp  42635  0prjspnrel  42650  dffltz  42657  eldiophb  42780  monotuz  42965  pwssplit4  43113  pwfi2f1o  43120  arearect  43239  cantnfresb  43348  omabs2  43356  fvnonrel  43621  rclexi  43639  rtrclex  43641  trclexi  43644  rtrclexi  43645  clcnvlem  43647  cnvrcl0  43649  cnvtrcl0  43650  dfrtrcl5  43653  dfrcl2  43698  comptiunov2i  43730  corclrcl  43731  trclrelexplem  43735  relexpaddss  43742  cotrcltrcl  43749  corcltrcl  43763  cotrclrcl  43766  frege131d  43788  0he  43806  grumnudlem  44309  uzmptshftfval  44370  binomcxplemdvbinom  44377  binomcxplemdvsum  44379  binomcxplemnotnn0  44380  modelaxreplem2  45004  rabexgf  45048  uzct  45087  disjf1o  45215  dmmptssf  45256  mptssid  45265  uzfissfz  45353  ssuzfz  45376  uzssre2  45434  uzublem  45457  uzssz2  45483  uzsscn2  45504  sumnnodd  45659  climconstmpt  45687  fnlimfvre  45703  fnlimabslt  45708  limsupvaluz  45737  limsupubuzlem  45741  limsupubuz  45742  limsupequzmpt2  45747  limsupmnfuzlem  45755  limsupre3uzlem  45764  liminfequzmpt2  45820  ibliooicc  46000  stoweidlem44  46073  stoweidlem50  46079  stoweidlem51  46080  stoweidlem52  46081  stoweidlem57  46086  stoweidlem59  46088  fourierdlem16  46152  fourierdlem19  46155  fourierdlem21  46157  fourierdlem22  46158  fourierdlem42  46178  fourierdlem83  46218  fouriersw  46260  salexct  46363  salexct3  46371  salgencntex  46372  salgensscntex  46373  sge0less  46421  sge0fodjrnlem  46445  sge0isum  46456  ovnlerp  46591  ovn0lem  46594  hoidmv1lelem1  46620  hoidmv1lelem3  46622  hoidmvlelem1  46624  hoidmvlelem2  46625  hoidmvlelem3  46626  hoidmvlelem4  46627  ovnhoilem1  46630  ovnhoilem2  46631  opnvonmbllem2  46662  ovolval4lem1  46678  ovolval5lem3  46683  pimdecfgtioc  46744  pimincfltioc  46745  pimdecfgtioo  46746  pimincfltioo  46747  incsmflem  46770  decsmflem  46795  smflimlem2  46801  smflimlem3  46802  smflim  46806  smfrec  46818  smfmullem4  46823  smfdiv  46826  smfsuplem1  46840  smfsuplem3  46842  smfsupxr  46845  smfliminflem  46859  cfsetssfset  47085  fcoreslem2  47093  fcores  47096  gricrel  47932  clnbgrisubgrgrim  47945  isubgr3stgrlem6  47983  isubgr3stgrlem7  47984  isubgr3stgrlem8  47985  isubgr3stgr  47987  grlimgrtrilem2  48007  grlicrel  48011  oddibas  48148  2zlidl  48215  2zrngbas  48217  2zrng0  48219  fldcALTV  48307  fldhmsubcALTV  48308  dmtposss  48851  tposres3  48856  ipolub0  48966  imaidfu  49069