Theorem eqsstri 3983

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

Syntax hints:   = wceq 1561   ⊆ wss 3905

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1816  ax-4 1830  ax-5 1931  ax-6 1988  ax-7 2029  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1801  df-cleq 2755  df-ss 3922

This theorem is referenced by:  eqsstrri  3984  3sstr4i  3988  ssrab3  4036  rabssab  4039  ifssun  4499  opabss  5165  brab2a  5741  relopabiALT  5797  dmopabss  5895  rnopabss  5932  resss  5988  relres  5992  rninOLD  6132  rnxpss  6159  cnvcnvss  6181  cnvcnvssOLD  6182  resdmss  6223  resssxp  6258  dfpo2  6284  predss  6297  fnres  6649  f0  6746  nfvres  6906  fvopab4ndm  7007  ffvresb  7108  mptexgf  7207  funiunfv  7233  isoini2  7324  ovssunirn  7433  dmoprabss  7501  mpondm0  7637  elmpocl  7638  exse2  7899  frxp  8107  tposssxp  8211  dftpos4  8226  smores  8324  smores2  8326  iordsmo  8329  swoer  8711  swoord1  8712  swoord2  8713  ecss  8731  ecopovsym  8802  ecopovtrn  8803  ecopover  8804  f1setex  8839  sbthlem7  9066  imafi  9260  elfiun  9377  marypha1lem  9380  marypha2lem1  9382  hartogslem1  9491  wdomima2g  9535  inf3lem1  9584  dmttrcl  9677  rnttrcl  9678  tc2  9696  frmin  9708  frrlem16  9717  frr1  9718  tz9.12lem1  9746  rankuni  9822  rankuniss  9825  rankmapu  9837  hta  9856  r0weon  9969  infxpenlem  9970  ackbij1lem9  10184  ackbij1lem10  10185  ackbij1b  10195  sdom2en01  10260  fin23lem26  10283  fin56  10351  fin1a2lem9  10366  axdc3lem  10408  axdc3lem2  10409  axcclem  10415  imadomg  10492  iundom2g  10498  smobeth  10545  canth4  10606  gruina  10777  grur1a  10778  pinn  10837  niex  10840  ltsopi  10847  ltrelpi  10848  dmaddpi  10849  dmmulpi  10850  enqex  10881  ltrelnq  10885  nqerf  10889  nqerrel  10891  dmrecnq  10927  lterpq  10929  ltrelpr  10957  enrex  11026  ltrelsr  11027  dmaddsr  11044  dmmulsr  11045  ltrelre  11093  axaddf  11104  axmulf  11105  ltrelxr  11244  lerelxr  11246  nn0ssre  12486  nn0sscn  12487  nn0ssz  12592  uzsupss  12942  rpnnen1lem1  12980  rpnnen1lem3  12981  rpnnen1lem5  12983  fz1ssfz0  13629  uzsup  13874  fzfi  13986  swrd00  14659  01sqrexlem3  15272  cau3  15384  caubnd  15387  limsupgre  15509  rlimpm  15528  rlimclim  15574  isercolllem1  15693  isercolllem2  15694  isercoll  15696  caurcvg  15705  caucvg  15707  iseraltlem2  15711  iseraltlem3  15712  zsum  15746  fsumcvg3  15757  climfsum  15849  ackbijnn  15859  divcnvshft  15886  infcvgaux1i  15888  clim2prod  15919  ntrivcvg  15928  ntrivcvgfvn0  15930  ntrivcvgtail  15931  ntrivcvgmullem  15932  ntrivcvgmul  15933  zprod  15968  dvdszrcl  16292  4sqlem1  16985  4sqlem19  17000  ramub1lem2  17064  structcnvcnv  17190  strleun  17194  fvsetsid  17205  smndex1sgrp  18946  gicer  19318  cntzsgrpcl  19375  symgbasfi  19420  mvdco  19486  symgsssg  19508  efglem  19757  efgtf  19763  efgtlen  19767  efginvrel2  19768  efginvrel1  19769  efgsfo  19780  efgredlemg  19783  efgredleme  19784  efgredlemd  19785  efgredlemc  19786  efgredlem  19788  efgred  19789  efgrelexlemb  19791  efgcpbllemb  19796  frgpinv  19805  frgpuplem  19813  frgpupf  19814  frgpup1  19816  frgpnabllem2  19915  gsumval3lem1  19946  gsumval3lem2  19947  gsumval3  19948  fldc  20834  fldhmsubc  20835  lbsextlem3  21231  pzriprnglem10  21543  znf1o  21604  zntoslem  21609  pjpm  21761  mhp0cl  22212  ply1bascl  22266  dmtopon  22984  ordtbas  23253  leordtval2  23273  lecldbas  23280  lmfval  23293  lmbrf  23321  cnconst2  23344  conncompcld  23495  hauspwdom  23562  txuni2  23626  xkouni  23660  xkoccn  23680  txkgen  23713  qtoptop2  23760  kqdisj  23793  hmphtop  23839  hmpher  23845  uzrest  23958  uzfbas  23959  lmflf  24066  tgpconncompeqg  24173  tgpconncomp  24174  ustn0  24282  xmeter  24494  isngp2  24658  xrtgioo  24868  iccntr  24883  xmetdcn  24900  metdcn  24902  metdscn2  24919  cnheiborlem  25017  reparphti  25060  lmmbrf  25325  iscau4  25342  iscauf  25343  caucfil  25346  lmclimf  25367  volf  25592  uniioombllem3  25648  uniioombllem4  25649  uniioombllem5  25650  volcn  25669  mbfimaopnlem  25718  mbflimsup  25729  i1f1  25753  itg2lcl  25790  itgioo  25879  itgsplitioo  25901  limcflflem  25943  limcflf  25944  limcresi  25948  lhop  26079  dvfsumlem1  26089  dvfsumlem2  26090  dvfsumlem3  26091  dvfsumlem4  26092  dvfsumrlimge0  26093  dvfsumrlim  26094  dvfsumrlim2  26095  dvfsum2  26097  vieta1lem1  26375  vieta1lem2  26376  psercnlem2  26488  psercnlem1  26489  psercn  26490  pserdvlem1  26491  pserdvlem2  26492  pserdv  26493  pserdv2  26494  logcnlem5  26712  dvlog  26717  dvlog2lem  26718  dvlog2  26719  dvcncxp1  26809  dvcnsqrt  26810  cxpcn3lem  26813  cxpcn3  26814  sqrtcn  26816  1cubr  26908  atansssdm  26999  jensen  27054  musum  27256  ppiub  27269  lgsquadlem1  27445  lgsquadlem2  27446  lgsquadlem3  27447  2sqlem7  27489  nosupbnd1lem1  27773  nosupbnd2  27781  noinfbnd1lem1  27788  cutsf  27886  leftssold  27965  rightssold  27966  mulsproplem12  28221  mulsproplem13  28222  mulsproplem14  28223  precsexlem8  28308  onssno  28348  nnssn0s  28415  dfnns2  28466  bdaypw2n0bndlem  28557  axtgcgrrflx  28632  axtgcgrid  28633  axtgsegcon  28634  axtg5seg  28635  axtgbtwnid  28636  axtgpasch  28637  axtgcont1  28638  tglng  28716  disjxwwlkn  30114  frgrwopreg2  30522  phnv  31018  htthlem  31121  hlimadd  31397  hlimcaui  31440  hhsscms  31482  occllem  31507  shjshsi  31696  3oalem4  31869  pjfi  31908  dmadjss  32091  nlelshi  32264  nlelchi  32265  hmopidmchi  32355  shatomistici  32565  difxp1ss  32722  difxp2ss  32723  fcoinver  32805  opabssi  32816  mptctf  32919  ccatws1f1o  33130  gsumpart  33244  pmtrcnel2  33271  psgnfzto1stlem  33281  cycpmrn  33324  cyc3genpm  33333  unitprodclb  33576  lsmsnorb  33578  ply1degltel  33791  ply1degleel  33792  ply1degltlss  33793  evlextv  33840  vietalem  33877  constrsscn  34038  cnre2csqima  34209  raddcn  34227  zrhcntr  34277  rrhre  34319  esumsnf  34362  sxbrsiga  34588  omssubadd  34598  carsggect  34616  sitmcl  34649  oddpwdc  34652  eulerpartlem1  34665  eulerpartlemt  34669  eulerpartgbij  34670  eulerpartlemmf  34673  eulerpartlemgh  34676  sseqf  34690  ballotlemfmpn  34793  ballotth  34836  signswch  34856  ftc2re  34893  fdvposlt  34894  fdvposle  34896  bnj1146  35087  bnj1292  35111  bnj1293  35112  bnj1145  35289  bnj1177  35302  fineqvnttrclse  35421  tz9.1regs  35431  erdszelem2  35543  kur14lem3  35559  kur14lem6  35562  kur14lem7  35563  kur14lem9  35565  cvmlift2lem12  35665  mpstssv  35890  mstapst  35898  mppspstlem  35922  mppspst  35925  mthmsta  35929  mthmpps  35933  mclsppslem  35934  txpss3v  36227  pprodss4v  36233  relsset  36237  fixssdm  36255  fixssrn  36256  limitssson  36260  funpartss  36295  colinearex  36411  fneer  36714  neibastop1  36720  neibastop2lem  36721  filnetlem2  36740  filnetlem3  36741  ttcuniun  36871  ttcuni  36874  knoppcnlem10  36941  bj-tagss  37466  bj-imdirco  37683  bj-fvsnun2  37749  bj-ablssgrp  37769  bj-ablsscmn  37771  bj-vecssmod  37774  bj-fldssdrng  37781  icoreresf  37847  icoreunrn  37854  poimirlem29  38149  poimirlem30  38150  poimirlem31  38151  poimir  38153  broucube  38154  dvasin  38204  dvacos  38205  areacirc  38213  caures  38260  bnd2lem  38291  ismtyres  38308  flddivrng  38499  xrnss3v  38881  refrelsredund2  39217  toycom  39598  dihglblem2N  41919  lcdvbase  42218  mapdunirnN  42275  aks6d1c1p1rcl  42726  redvmptabs  42970  readvrec  42972  prjspreln0  43192  prjspvs  43193  prjspeclsp  43195  0prjspnrel  43210  dffltz  43217  eldiophb  43339  monotuz  43519  pwssplit4  43667  pwfi2f1o  43674  arearect  43793  cantnfresb  43902  omabs2  43910  fvnonrel  44174  rclexi  44192  rtrclex  44194  trclexi  44197  rtrclexi  44198  clcnvlem  44200  cnvrcl0  44202  cnvtrcl0  44203  dfrtrcl5  44206  dfrcl2  44251  comptiunov2i  44283  corclrcl  44284  trclrelexplem  44288  relexpaddss  44295  cotrcltrcl  44302  corcltrcl  44316  cotrclrcl  44319  frege131d  44341  0he  44359  grumnudlem  44862  uzmptshftfval  44923  binomcxplemdvbinom  44930  binomcxplemdvsum  44932  binomcxplemnotnn0  44933  modelaxreplem2  45556  rabexgf  45605  uzct  45644  disjf1o  45770  dmmptssf  45808  mptssid  45817  uzfissfz  45903  ssuzfz  45926  uzssre2  45982  uzublem  46005  uzssz2  46031  uzsscn2  46052  sumnnodd  46207  climconstmpt  46233  fnlimfvre  46249  fnlimabslt  46254  limsupubuzlem  46287  limsupubuz  46288  limsupequzmpt2  46293  limsupmnfuzlem  46301  limsupre3uzlem  46310  liminfequzmpt2  46366  ibliooicc  46546  stoweidlem44  46619  stoweidlem50  46625  stoweidlem51  46626  stoweidlem52  46627  stoweidlem57  46632  stoweidlem59  46634  fourierdlem16  46698  fourierdlem19  46701  fourierdlem21  46703  fourierdlem22  46704  fourierdlem42  46724  fourierdlem83  46764  fouriersw  46806  salexct  46909  salexct3  46917  salgencntex  46918  salgensscntex  46919  sge0less  46967  sge0fodjrnlem  46991  sge0isum  47002  ovnlerp  47137  ovn0lem  47140  hoidmv1lelem1  47166  hoidmv1lelem3  47168  hoidmvlelem1  47170  hoidmvlelem2  47171  hoidmvlelem3  47172  hoidmvlelem4  47173  ovnhoilem1  47176  ovnhoilem2  47177  opnvonmbllem2  47208  ovolval4lem1  47224  ovolval5lem3  47229  pimdecfgtioc  47290  pimincfltioc  47291  pimdecfgtioo  47292  pimincfltioo  47293  incsmflem  47316  decsmflem  47341  smflimlem2  47347  smflimlem3  47348  smflim  47352  smfrec  47364  smfmullem4  47369  smfdiv  47372  smfsuplem1  47386  smfsuplem3  47388  smfsupxr  47391  smfliminflem  47405  cfsetssfset  47651  fcoreslem2  47659  fcores  47662  gricrel  48542  clnbgrisubgrgrim  48555  isubgr3stgrlem6  48594  isubgr3stgrlem7  48595  isubgr3stgrlem8  48596  isubgr3stgr  48598  grlimgrtrilem2  48625  grlicrel  48629  oddibas  48796  2zlidl  48863  2zrngbas  48865  2zrng0  48867  fldcALTV  48955  fldhmsubcALTV  48956  dmtposss  49498  tposres3  49503  ipolub0  49614  imaidfu  49732