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  5725  relopabiALT  5780  dmopabss  5875  rnopabss  5912  resss  5968  relres  5972  rnin  6112  rnxpss  6138  cnvcnvss  6160  resdmss  6201  resssxp  6236  dfpo2  6262  predss  6275  fnres  6627  f0  6723  nfvres  6880  fvopab4ndm  6980  ffvresb  7080  mptexgf  7178  funiunfv  7204  isoini2  7295  ovssunirn  7404  dmoprabss  7472  mpondm0  7608  elmpocl  7609  exse2  7869  fabexgOLD  7891  frxp  8078  tposssxp  8182  dftpos4  8197  smores  8294  smores2  8296  iordsmo  8299  swoer  8677  swoord1  8678  swoord2  8679  ecss  8697  ecopovsym  8768  ecopovtrn  8769  ecopover  8770  f1setex  8806  sbthlem7  9033  imafi  9227  elfiun  9345  marypha1lem  9348  marypha2lem1  9350  hartogslem1  9459  wdomima2g  9503  inf3lem1  9549  dmttrcl  9642  rnttrcl  9643  tc2  9661  frmin  9673  frrlem16  9682  frr1  9683  tz9.12lem1  9711  rankuni  9787  rankuniss  9790  rankmapu  9802  hta  9821  r0weon  9934  infxpenlem  9935  ackbij1lem9  10149  ackbij1lem10  10150  ackbij1b  10160  sdom2en01  10224  fin23lem26  10247  fin56  10315  fin1a2lem9  10330  axdc3lem  10372  axdc3lem2  10373  axcclem  10379  imadomg  10456  iundom2g  10462  smobeth  10509  canth4  10570  gruina  10741  grur1a  10742  pinn  10801  niex  10804  ltsopi  10811  ltrelpi  10812  dmaddpi  10813  dmmulpi  10814  enqex  10845  ltrelnq  10849  nqerf  10853  nqerrel  10855  dmrecnq  10891  lterpq  10893  ltrelpr  10921  enrex  10990  ltrelsr  10991  dmaddsr  11008  dmmulsr  11009  ltrelre  11057  axaddf  11068  axmulf  11069  ltrelxr  11205  lerelxr  11207  nn0ssre  12417  nn0sscn  12418  nn0ssz  12523  uzsupss  12865  rpnnen1lem1  12903  rpnnen1lem3  12904  rpnnen1lem5  12906  fz1ssfz0  13551  uzsup  13795  fzfi  13907  swrd00  14580  01sqrexlem3  15179  cau3  15291  caubnd  15294  limsupgre  15416  rlimpm  15435  rlimclim  15481  isercolllem1  15600  isercolllem2  15601  isercoll  15603  caurcvg  15612  caucvg  15614  iseraltlem2  15618  iseraltlem3  15619  zsum  15653  fsumcvg3  15664  climfsum  15755  ackbijnn  15763  divcnvshft  15790  infcvgaux1i  15792  clim2prod  15823  ntrivcvg  15832  ntrivcvgfvn0  15834  ntrivcvgtail  15835  ntrivcvgmullem  15836  ntrivcvgmul  15837  zprod  15872  dvdszrcl  16196  4sqlem1  16888  4sqlem19  16903  ramub1lem2  16967  structcnvcnv  17092  strleun  17096  fvsetsid  17107  smndex1sgrp  18845  gicer  19218  cntzsgrpcl  19275  symgbasfi  19320  mvdco  19386  symgsssg  19408  efglem  19657  efgtf  19663  efgtlen  19667  efginvrel2  19668  efginvrel1  19669  efgsfo  19680  efgredlemg  19683  efgredleme  19684  efgredlemd  19685  efgredlemc  19686  efgredlem  19688  efgred  19689  efgrelexlemb  19691  efgcpbllemb  19696  frgpinv  19705  frgpuplem  19713  frgpupf  19714  frgpup1  19716  frgpnabllem2  19815  gsumval3lem1  19846  gsumval3lem2  19847  gsumval3  19848  fldc  20729  fldhmsubc  20730  lbsextlem3  21127  pzriprnglem10  21457  znf1o  21518  zntoslem  21523  pjpm  21675  mhp0cl  22101  ply1bascl  22156  dmtopon  22879  ordtbas  23148  leordtval2  23168  lecldbas  23175  lmfval  23188  lmbrf  23216  cnconst2  23239  conncompcld  23390  hauspwdom  23457  txuni2  23521  xkouni  23555  xkoccn  23575  txkgen  23608  qtoptop2  23655  kqdisj  23688  hmphtop  23734  hmpher  23740  uzrest  23853  uzfbas  23854  lmflf  23961  tgpconncompeqg  24068  tgpconncomp  24069  ustn0  24177  xmeter  24389  isngp2  24553  xrtgioo  24763  iccntr  24778  xmetdcn  24795  metdcn  24797  metdscn2  24814  icchmeoOLD  24907  cnheiborlem  24921  reparphti  24964  lmmbrf  25230  iscau4  25247  iscauf  25248  caucfil  25251  lmclimf  25272  volf  25498  uniioombllem3  25554  uniioombllem4  25555  uniioombllem5  25556  volcn  25575  mbfimaopnlem  25624  mbflimsup  25635  i1f1  25659  itg2lcl  25696  itgioo  25785  itgsplitioo  25807  limcflflem  25849  limcflf  25850  limcresi  25854  lhop  25989  dvfsumlem1  26000  dvfsumlem2  26001  dvfsumlem2OLD  26002  dvfsumlem3  26003  dvfsumlem4  26004  dvfsumrlimge0  26005  dvfsumrlim  26006  dvfsumrlim2  26007  dvfsum2  26009  vieta1lem1  26286  vieta1lem2  26287  psercnlem2  26402  psercnlem1  26403  psercn  26404  pserdvlem1  26405  pserdvlem2  26406  pserdv  26407  pserdv2  26408  logcnlem5  26623  dvlog  26628  dvlog2lem  26629  dvlog2  26630  dvcncxp1  26720  dvcnsqrt  26721  cxpcn3lem  26725  cxpcn3  26726  sqrtcn  26728  1cubr  26820  atansssdm  26911  jensen  26967  musum  27169  ppiub  27183  lgsquadlem1  27359  lgsquadlem2  27360  lgsquadlem3  27361  2sqlem7  27403  nosupbnd1lem1  27688  nosupbnd2  27696  noinfbnd1lem1  27703  cutsf  27800  leftssold  27879  rightssold  27880  mulsproplem12  28135  mulsproplem13  28136  mulsproplem14  28137  precsexlem8  28222  onssno  28262  nnssn0s  28329  dfnns2  28380  bdaypw2n0bndlem  28471  axtgcgrrflx  28546  axtgcgrid  28547  axtgsegcon  28548  axtg5seg  28549  axtgbtwnid  28550  axtgpasch  28551  axtgcont1  28552  tglng  28630  disjxwwlkn  29998  frgrwopreg2  30406  phnv  30902  htthlem  31005  hlimadd  31281  hlimcaui  31324  hhsscms  31366  occllem  31391  shjshsi  31580  3oalem4  31753  pjfi  31792  dmadjss  31975  nlelshi  32148  nlelchi  32149  hmopidmchi  32239  shatomistici  32449  difxp1ss  32609  difxp2ss  32610  fcoinver  32691  opabssi  32703  mptctf  32806  ccatws1f1o  33044  gsumpart  33157  pmtrcnel2  33184  psgnfzto1stlem  33194  cycpmrn  33237  cyc3genpm  33246  unitprodclb  33482  lsmsnorb  33484  ply1degltel  33687  ply1degleel  33688  ply1degltlss  33689  evlextv  33719  vietalem  33756  constrsscn  33918  cnre2csqima  34089  raddcn  34107  zrhcntr  34157  rrhre  34199  esumsnf  34242  sxbrsiga  34468  omssubadd  34478  carsggect  34496  sitmcl  34529  oddpwdc  34532  eulerpartlem1  34545  eulerpartlemt  34549  eulerpartgbij  34550  eulerpartlemmf  34553  eulerpartlemgh  34556  sseqf  34570  ballotlemfmpn  34673  ballotth  34716  signswch  34739  ftc2re  34776  fdvposlt  34777  fdvposle  34779  bnj1146  34967  bnj1292  34991  bnj1293  34992  bnj1145  35169  bnj1177  35182  fineqvnttrclse  35302  tz9.1regs  35312  erdszelem2  35408  kur14lem3  35424  kur14lem6  35427  kur14lem7  35428  kur14lem9  35430  cvmlift2lem12  35530  mpstssv  35755  mstapst  35763  mppspstlem  35787  mppspst  35790  mthmsta  35794  mthmpps  35798  mclsppslem  35799  txpss3v  36092  pprodss4v  36098  relsset  36102  fixssdm  36120  fixssrn  36121  limitssson  36125  funpartss  36160  colinearex  36276  fneer  36569  neibastop1  36575  neibastop2lem  36576  filnetlem2  36595  filnetlem3  36596  knoppcnlem10  36724  bj-tagss  37228  bj-imdirco  37445  bj-fvsnun2  37511  bj-ablssgrp  37531  bj-ablsscmn  37533  bj-vecssmod  37536  bj-fldssdrng  37543  icoreresf  37607  icoreunrn  37614  poimirlem29  37900  poimirlem30  37901  poimirlem31  37902  poimir  37904  broucube  37905  dvasin  37955  dvacos  37956  areacirc  37964  caures  38011  bnd2lem  38042  ismtyres  38059  flddivrng  38250  xrnss3v  38632  refrelsredund2  38968  toycom  39349  dihglblem2N  41670  lcdvbase  41969  mapdunirnN  42026  aks6d1c1p1rcl  42478  redvmptabs  42730  readvrec  42732  prjspreln0  42967  prjspvs  42968  prjspeclsp  42970  0prjspnrel  42985  dffltz  42992  eldiophb  43114  monotuz  43298  pwssplit4  43446  pwfi2f1o  43453  arearect  43572  cantnfresb  43681  omabs2  43689  fvnonrel  43953  rclexi  43971  rtrclex  43973  trclexi  43976  rtrclexi  43977  clcnvlem  43979  cnvrcl0  43981  cnvtrcl0  43982  dfrtrcl5  43985  dfrcl2  44030  comptiunov2i  44062  corclrcl  44063  trclrelexplem  44067  relexpaddss  44074  cotrcltrcl  44081  corcltrcl  44095  cotrclrcl  44098  frege131d  44120  0he  44138  grumnudlem  44641  uzmptshftfval  44702  binomcxplemdvbinom  44709  binomcxplemdvsum  44711  binomcxplemnotnn0  44712  modelaxreplem2  45335  rabexgf  45384  uzct  45423  disjf1o  45550  dmmptssf  45590  mptssid  45599  uzfissfz  45685  ssuzfz  45708  uzssre2  45765  uzublem  45788  uzssz2  45814  uzsscn2  45835  sumnnodd  45990  climconstmpt  46016  fnlimfvre  46032  fnlimabslt  46037  limsupvaluz  46066  limsupubuzlem  46070  limsupubuz  46071  limsupequzmpt2  46076  limsupmnfuzlem  46084  limsupre3uzlem  46093  liminfequzmpt2  46149  ibliooicc  46329  stoweidlem44  46402  stoweidlem50  46408  stoweidlem51  46409  stoweidlem52  46410  stoweidlem57  46415  stoweidlem59  46417  fourierdlem16  46481  fourierdlem19  46484  fourierdlem21  46486  fourierdlem22  46487  fourierdlem42  46507  fourierdlem83  46547  fouriersw  46589  salexct  46692  salexct3  46700  salgencntex  46701  salgensscntex  46702  sge0less  46750  sge0fodjrnlem  46774  sge0isum  46785  ovnlerp  46920  ovn0lem  46923  hoidmv1lelem1  46949  hoidmv1lelem3  46951  hoidmvlelem1  46953  hoidmvlelem2  46954  hoidmvlelem3  46955  hoidmvlelem4  46956  ovnhoilem1  46959  ovnhoilem2  46960  opnvonmbllem2  46991  ovolval4lem1  47007  ovolval5lem3  47012  pimdecfgtioc  47073  pimincfltioc  47074  pimdecfgtioo  47075  pimincfltioo  47076  incsmflem  47099  decsmflem  47124  smflimlem2  47130  smflimlem3  47131  smflim  47135  smfrec  47147  smfmullem4  47152  smfdiv  47155  smfsuplem1  47169  smfsuplem3  47171  smfsupxr  47174  smfliminflem  47188  cfsetssfset  47416  fcoreslem2  47424  fcores  47427  gricrel  48279  clnbgrisubgrgrim  48292  isubgr3stgrlem6  48331  isubgr3stgrlem7  48332  isubgr3stgrlem8  48333  isubgr3stgr  48335  grlimgrtrilem2  48362  grlicrel  48366  oddibas  48533  2zlidl  48600  2zrngbas  48602  2zrng0  48604  fldcALTV  48692  fldhmsubcALTV  48693  dmtposss  49235  tposres3  49240  ipolub0  49351  imaidfu  49469