Theorem eqsstri 3990

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

Syntax hints:   = wceq 1540   ⊆ wss 3911

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 2701

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

This theorem is referenced by:  eqsstrri  3991  3sstr4i  3995  ssrab3  4041  rabssab  4044  ifssun  4502  opabss  5166  brab2a  5724  relopabiALT  5777  dmopabss  5872  rnopabss  5908  resss  5961  relres  5965  rnin  6107  rnxpss  6133  cnvcnvss  6155  resdmss  6196  resssxp  6231  dfpo2  6257  predss  6270  fnres  6627  f0  6723  nfvres  6881  fvopab4ndm  6980  ffvresb  7079  mptexgf  7178  funiunfv  7204  isoini2  7296  ovssunirn  7405  dmoprabss  7473  mpondm0  7609  elmpocl  7610  exse2  7873  fabexgOLD  7895  frxp  8082  tposssxp  8186  dftpos4  8201  smores  8298  smores2  8300  iordsmo  8303  swoer  8679  swoord1  8680  swoord2  8681  ecss  8699  ecopovsym  8769  ecopovtrn  8770  ecopover  8771  f1setex  8807  sbthlem7  9034  imafi  9240  elfiun  9357  marypha1lem  9360  marypha2lem1  9362  hartogslem1  9471  wdomima2g  9515  inf3lem1  9557  dmttrcl  9650  rnttrcl  9651  tc2  9671  frmin  9678  frrlem16  9687  frr1  9688  tz9.12lem1  9716  rankuni  9792  rankuniss  9795  rankmapu  9807  hta  9826  r0weon  9941  infxpenlem  9942  ackbij1lem9  10156  ackbij1lem10  10157  ackbij1b  10167  sdom2en01  10231  fin23lem26  10254  fin56  10322  fin1a2lem9  10337  axdc3lem  10379  axdc3lem2  10380  axcclem  10386  imadomg  10463  iundom2g  10469  smobeth  10515  canth4  10576  gruina  10747  grur1a  10748  pinn  10807  niex  10810  ltsopi  10817  ltrelpi  10818  dmaddpi  10819  dmmulpi  10820  enqex  10851  ltrelnq  10855  nqerf  10859  nqerrel  10861  dmrecnq  10897  lterpq  10899  ltrelpr  10927  enrex  10996  ltrelsr  10997  dmaddsr  11014  dmmulsr  11015  ltrelre  11063  axaddf  11074  axmulf  11075  ltrelxr  11211  lerelxr  11213  nn0ssre  12422  nn0sscn  12423  nn0ssz  12528  uzsupss  12875  rpnnen1lem1  12913  rpnnen1lem3  12914  rpnnen1lem5  12916  fz1ssfz0  13560  uzsup  13801  fzfi  13913  swrd00  14585  01sqrexlem3  15186  cau3  15298  caubnd  15301  limsupgre  15423  rlimpm  15442  rlimclim  15488  isercolllem1  15607  isercolllem2  15608  isercoll  15610  caurcvg  15619  caucvg  15621  iseraltlem2  15625  iseraltlem3  15626  zsum  15660  fsumcvg3  15671  climfsum  15762  ackbijnn  15770  divcnvshft  15797  infcvgaux1i  15799  clim2prod  15830  ntrivcvg  15839  ntrivcvgfvn0  15841  ntrivcvgtail  15842  ntrivcvgmullem  15843  ntrivcvgmul  15844  zprod  15879  dvdszrcl  16203  4sqlem1  16895  4sqlem19  16910  ramub1lem2  16974  structcnvcnv  17099  strleun  17103  fvsetsid  17114  smndex1sgrp  18811  gicer  19185  cntzsgrpcl  19242  symgbasfi  19285  mvdco  19351  symgsssg  19373  efglem  19622  efgtf  19628  efgtlen  19632  efginvrel2  19633  efginvrel1  19634  efgsfo  19645  efgredlemg  19648  efgredleme  19649  efgredlemd  19650  efgredlemc  19651  efgredlem  19653  efgred  19654  efgrelexlemb  19656  efgcpbllemb  19661  frgpinv  19670  frgpuplem  19678  frgpupf  19679  frgpup1  19681  frgpnabllem2  19780  gsumval3lem1  19811  gsumval3lem2  19812  gsumval3  19813  fldc  20669  fldhmsubc  20670  lbsextlem3  21046  pzriprnglem10  21376  znf1o  21437  zntoslem  21442  pjpm  21593  mhp0cl  22009  ply1bascl  22064  dmtopon  22786  ordtbas  23055  leordtval2  23075  lecldbas  23082  lmfval  23095  lmbrf  23123  cnconst2  23146  conncompcld  23297  hauspwdom  23364  txuni2  23428  xkouni  23462  xkoccn  23482  txkgen  23515  qtoptop2  23562  kqdisj  23595  hmphtop  23641  hmpher  23647  uzrest  23760  uzfbas  23761  lmflf  23868  tgpconncompeqg  23975  tgpconncomp  23976  ustn0  24084  xmeter  24297  isngp2  24461  xrtgioo  24671  iccntr  24686  xmetdcn  24703  metdcn  24705  metdscn2  24722  icchmeoOLD  24815  cnheiborlem  24829  reparphti  24872  lmmbrf  25138  iscau4  25155  iscauf  25156  caucfil  25159  lmclimf  25180  volf  25406  uniioombllem3  25462  uniioombllem4  25463  uniioombllem5  25464  volcn  25483  mbfimaopnlem  25532  mbflimsup  25543  i1f1  25567  itg2lcl  25604  itgioo  25693  itgsplitioo  25715  limcflflem  25757  limcflf  25758  limcresi  25762  lhop  25897  dvfsumlem1  25908  dvfsumlem2  25909  dvfsumlem2OLD  25910  dvfsumlem3  25911  dvfsumlem4  25912  dvfsumrlimge0  25913  dvfsumrlim  25914  dvfsumrlim2  25915  dvfsum2  25917  vieta1lem1  26194  vieta1lem2  26195  psercnlem2  26310  psercnlem1  26311  psercn  26312  pserdvlem1  26313  pserdvlem2  26314  pserdv  26315  pserdv2  26316  logcnlem5  26531  dvlog  26536  dvlog2lem  26537  dvlog2  26538  dvcncxp1  26628  dvcnsqrt  26629  cxpcn3lem  26633  cxpcn3  26634  sqrtcn  26636  1cubr  26728  atansssdm  26819  jensen  26875  musum  27077  ppiub  27091  lgsquadlem1  27267  lgsquadlem2  27268  lgsquadlem3  27269  2sqlem7  27311  nosupbnd1lem1  27596  nosupbnd2  27604  noinfbnd1lem1  27611  scutf  27700  leftssold  27766  rightssold  27767  mulsproplem12  28006  mulsproplem13  28007  mulsproplem14  28008  precsexlem8  28092  onssno  28131  nnssn0s  28190  dfnns2  28237  axtgcgrrflx  28365  axtgcgrid  28366  axtgsegcon  28367  axtg5seg  28368  axtgbtwnid  28369  axtgpasch  28370  axtgcont1  28371  tglng  28449  disjxwwlkn  29816  frgrwopreg2  30221  phnv  30716  htthlem  30819  hlimadd  31095  hlimcaui  31138  hhsscms  31180  occllem  31205  shjshsi  31394  3oalem4  31567  pjfi  31606  dmadjss  31789  nlelshi  31962  nlelchi  31963  hmopidmchi  32053  shatomistici  32263  difxp1ss  32424  difxp2ss  32425  fcoinver  32506  opabssi  32514  mptctf  32614  ccatws1f1o  32846  gsumpart  32970  pmtrcnel2  33020  psgnfzto1stlem  33030  cycpmrn  33073  cyc3genpm  33082  unitprodclb  33333  lsmsnorb  33335  ply1degltel  33533  ply1degleel  33534  ply1degltlss  33535  constrsscn  33703  cnre2csqima  33874  raddcn  33892  zrhcntr  33942  rrhre  33984  esumsnf  34027  sxbrsiga  34254  omssubadd  34264  carsggect  34282  sitmcl  34315  oddpwdc  34318  eulerpartlem1  34331  eulerpartlemt  34335  eulerpartgbij  34336  eulerpartlemmf  34339  eulerpartlemgh  34342  sseqf  34356  ballotlemfmpn  34459  ballotth  34502  signswch  34525  ftc2re  34562  fdvposlt  34563  fdvposle  34565  bnj1146  34754  bnj1292  34778  bnj1293  34779  bnj1145  34956  bnj1177  34969  erdszelem2  35152  kur14lem3  35168  kur14lem6  35171  kur14lem7  35172  kur14lem9  35174  cvmlift2lem12  35274  mpstssv  35499  mstapst  35507  mppspstlem  35531  mppspst  35534  mthmsta  35538  mthmpps  35542  mclsppslem  35543  txpss3v  35839  pprodss4v  35845  relsset  35849  fixssdm  35867  fixssrn  35868  limitssson  35872  funpartss  35905  colinearex  36021  fneer  36314  neibastop1  36320  neibastop2lem  36321  filnetlem2  36340  filnetlem3  36341  knoppcnlem10  36463  bj-tagss  36941  bj-imdirco  37151  bj-fvsnun2  37217  bj-ablssgrp  37237  bj-ablsscmn  37239  bj-vecssmod  37242  bj-fldssdrng  37249  icoreresf  37313  icoreunrn  37320  poimirlem29  37616  poimirlem30  37617  poimirlem31  37618  poimir  37620  broucube  37621  dvasin  37671  dvacos  37672  areacirc  37680  caures  37727  bnd2lem  37758  ismtyres  37775  flddivrng  37966  xrnss3v  38327  refrelsredund2  38597  toycom  38939  dihglblem2N  41261  lcdvbase  41560  mapdunirnN  41617  aks6d1c1p1rcl  42069  redvmptabs  42321  readvrec  42323  prjspreln0  42570  prjspvs  42571  prjspeclsp  42573  0prjspnrel  42588  dffltz  42595  eldiophb  42718  monotuz  42903  pwssplit4  43051  pwfi2f1o  43058  arearect  43177  cantnfresb  43286  omabs2  43294  fvnonrel  43559  rclexi  43577  rtrclex  43579  trclexi  43582  rtrclexi  43583  clcnvlem  43585  cnvrcl0  43587  cnvtrcl0  43588  dfrtrcl5  43591  dfrcl2  43636  comptiunov2i  43668  corclrcl  43669  trclrelexplem  43673  relexpaddss  43680  cotrcltrcl  43687  corcltrcl  43701  cotrclrcl  43704  frege131d  43726  0he  43744  grumnudlem  44247  uzmptshftfval  44308  binomcxplemdvbinom  44315  binomcxplemdvsum  44317  binomcxplemnotnn0  44318  modelaxreplem2  44942  rabexgf  44991  uzct  45030  disjf1o  45158  dmmptssf  45199  mptssid  45208  uzfissfz  45295  ssuzfz  45318  uzssre2  45376  uzublem  45399  uzssz2  45425  uzsscn2  45446  sumnnodd  45601  climconstmpt  45629  fnlimfvre  45645  fnlimabslt  45650  limsupvaluz  45679  limsupubuzlem  45683  limsupubuz  45684  limsupequzmpt2  45689  limsupmnfuzlem  45697  limsupre3uzlem  45706  liminfequzmpt2  45762  ibliooicc  45942  stoweidlem44  46015  stoweidlem50  46021  stoweidlem51  46022  stoweidlem52  46023  stoweidlem57  46028  stoweidlem59  46030  fourierdlem16  46094  fourierdlem19  46097  fourierdlem21  46099  fourierdlem22  46100  fourierdlem42  46120  fourierdlem83  46160  fouriersw  46202  salexct  46305  salexct3  46313  salgencntex  46314  salgensscntex  46315  sge0less  46363  sge0fodjrnlem  46387  sge0isum  46398  ovnlerp  46533  ovn0lem  46536  hoidmv1lelem1  46562  hoidmv1lelem3  46564  hoidmvlelem1  46566  hoidmvlelem2  46567  hoidmvlelem3  46568  hoidmvlelem4  46569  ovnhoilem1  46572  ovnhoilem2  46573  opnvonmbllem2  46604  ovolval4lem1  46620  ovolval5lem3  46625  pimdecfgtioc  46686  pimincfltioc  46687  pimdecfgtioo  46688  pimincfltioo  46689  incsmflem  46712  decsmflem  46737  smflimlem2  46743  smflimlem3  46744  smflim  46748  smfrec  46760  smfmullem4  46765  smfdiv  46768  smfsuplem1  46782  smfsuplem3  46784  smfsupxr  46787  smfliminflem  46801  cfsetssfset  47030  fcoreslem2  47038  fcores  47041  gricrel  47892  clnbgrisubgrgrim  47905  isubgr3stgrlem6  47943  isubgr3stgrlem7  47944  isubgr3stgrlem8  47945  isubgr3stgr  47947  grlimgrtrilem2  47967  grlicrel  47971  oddibas  48134  2zlidl  48201  2zrngbas  48203  2zrng0  48205  fldcALTV  48293  fldhmsubcALTV  48294  dmtposss  48837  tposres3  48842  ipolub0  48953  imaidfu  49072