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 234	1 ⊢ 𝐴 ⊆ 𝐶

Syntax hints:   = wceq 1570   ⊆ wss 3905

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-cleq 2755  df-ss 3922

This theorem is referenced by:  eqsstrri  3984  3sstr4i  3988  ssrab3  4036  rabssab  4039  ifssun  4505  opabss  5175  brab2a  5754  relopabiALT  5810  dmopabss  5908  rnopabss  5945  resss  6000  relres  6004  rninOLD  6144  rnxpss  6170  cnvcnvss  6192  cnvcnvssOLD  6193  resdmss  6236  resssxp  6271  dfpo2  6297  predss  6310  fnres  6662  f0  6759  nfvres  6919  fvopab4ndm  7020  ffvresb  7121  mptexgf  7220  funiunfv  7246  isoini2  7337  ovssunirn  7446  dmoprabss  7514  mpondm0  7650  elmpocl  7651  exse2  7910  frxp  8118  tposssxp  8222  dftpos4  8237  smores  8335  smores2  8337  iordsmo  8340  swoer  8722  swoord1  8723  swoord2  8724  ecss  8742  ecopovsym  8813  ecopovtrn  8814  ecopover  8815  f1setex  8850  sbthlem7  9077  imafi  9271  elfiun  9386  marypha1lem  9389  marypha2lem1  9391  hartogslem1  9500  wdomima2g  9544  inf3lem1  9593  dmttrcl  9686  rnttrcl  9687  tc2  9705  frmin  9717  frrlem16  9726  frr1  9727  tz9.12lem1  9755  rankuni  9831  rankuniss  9834  rankmapu  9846  hta  9879  r0weon  9992  infxpenlem  9993  ackbij1lem9  10206  ackbij1lem10  10207  ackbij1b  10217  sdom2en01  10281  fin23lem26  10304  fin56  10372  fin1a2lem9  10387  axdc3lem  10429  axdc3lem2  10430  axcclem  10436  imadomg  10513  iundom2g  10519  smobeth  10566  canth4  10627  gruina  10798  grur1a  10799  pinn  10858  niex  10861  ltsopi  10868  ltrelpi  10869  dmaddpi  10870  dmmulpi  10871  enqex  10902  ltrelnq  10906  nqerf  10910  nqerrel  10912  dmrecnq  10948  lterpq  10950  ltrelpr  10978  enrex  11047  ltrelsr  11048  dmaddsr  11065  dmmulsr  11066  ltrelre  11114  axaddf  11125  axmulf  11126  ltrelxr  11265  lerelxr  11267  nn0ssre  12503  nn0sscn  12504  nn0ssz  12609  uzsupss  12959  rpnnen1lem1  12997  rpnnen1lem3  12998  rpnnen1lem5  13000  fz1ssfz0  13647  uzsup  13892  fzfi  14004  swrd00  14678  01sqrexlem3  15291  cau3  15403  caubnd  15406  limsupgre  15528  rlimpm  15547  rlimclim  15593  isercolllem1  15712  isercolllem2  15713  isercoll  15715  caurcvg  15724  caucvg  15726  iseraltlem2  15730  iseraltlem3  15731  zsum  15765  fsumcvg3  15776  climfsum  15868  ackbijnn  15878  divcnvshft  15905  infcvgaux1i  15907  clim2prod  15938  ntrivcvg  15947  ntrivcvgfvn0  15949  ntrivcvgtail  15950  ntrivcvgmullem  15951  ntrivcvgmul  15952  zprod  15987  dvdszrcl  16310  4sqlem1  17003  4sqlem19  17018  ramub1lem2  17082  structcnvcnv  17208  strleun  17212  fvsetsid  17223  smndex1sgrp  18965  gicer  19342  cntzsgrpcl  19399  symgbasfi  19444  mvdco  19510  symgsssg  19532  efglem  19781  efgtf  19787  efgtlen  19791  efginvrel2  19792  efginvrel1  19793  efgsfo  19804  efgredlemg  19807  efgredleme  19808  efgredlemd  19809  efgredlemc  19810  efgredlem  19812  efgred  19813  efgrelexlemb  19815  efgcpbllemb  19820  frgpinv  19829  frgpuplem  19837  frgpupf  19838  frgpup1  19840  frgpnabllem2  19939  gsumval3lem1  19970  gsumval3lem2  19971  gsumval3  19972  ricrel  20592  fldc  20887  fldhmsubc  20888  lbsextlem3  21284  pzriprnglem10  21640  znf1o  21701  zntoslem  21706  pjpm  21858  mhp0cl  22309  ply1bascl  22363  dmtopon  23080  ordtbas  23349  leordtval2  23369  lecldbas  23376  lmfval  23389  lmbrf  23417  cnconst2  23440  conncompcld  23591  hauspwdom  23658  txuni2  23722  xkouni  23756  xkoccn  23776  txkgen  23809  qtoptop2  23856  kqdisj  23889  hmphtop  23935  hmpher  23941  uzrest  24054  uzfbas  24055  lmflf  24162  tgpconncompeqg  24269  tgpconncomp  24270  ustn0  24378  xmeter  24590  isngp2  24754  xrtgioo  24964  iccntr  24979  xmetdcn  24996  metdcn  24998  metdscn2  25015  cnheiborlem  25113  reparphti  25156  lmmbrf  25421  iscau4  25438  iscauf  25439  caucfil  25442  lmclimf  25463  volf  25688  uniioombllem3  25744  uniioombllem4  25745  uniioombllem5  25746  volcn  25765  mbfimaopnlem  25814  mbflimsup  25825  i1f1  25849  itg2lcl  25886  itgioo  25975  itgsplitioo  25997  limcflflem  26039  limcflf  26040  limcresi  26044  lhop  26175  dvfsumlem1  26185  dvfsumlem2  26186  dvfsumlem3  26187  dvfsumlem4  26188  dvfsumrlimge0  26189  dvfsumrlim  26190  dvfsumrlim2  26191  dvfsum2  26193  vieta1lem1  26471  vieta1lem2  26472  psercnlem2  26587  psercnlem1  26588  psercn  26589  pserdvlem1  26590  pserdvlem2  26591  pserdv  26592  pserdv2  26593  logcnlem5  26811  dvlog  26816  dvlog2lem  26817  dvlog2  26818  dvcncxp1  26908  dvcnsqrt  26909  cxpcn3lem  26912  cxpcn3  26913  sqrtcn  26915  1cubr  27007  atansssdm  27098  jensen  27153  musum  27355  ppiub  27368  lgsquadlem1  27544  lgsquadlem2  27545  lgsquadlem3  27546  2sqlem7  27588  nosupbnd1lem1  27872  nosupbnd2  27880  noinfbnd1lem1  27887  cutsf  27985  leftssold  28064  rightssold  28065  mulsproplem12  28320  mulsproplem13  28321  mulsproplem14  28322  precsexlem8  28407  onssno  28447  nnssn0s  28514  dfnns2  28565  bdaypw2n0bndlem  28656  axtgcgrrflx  28731  axtgcgrid  28732  axtgsegcon  28733  axtg5seg  28734  axtgbtwnid  28735  axtgpasch  28736  axtgcont1  28737  tglng  28815  disjxwwlkn  30262  frgrwopreg2  30670  phnv  31166  htthlem  31269  hlimadd  31545  hlimcaui  31588  hhsscms  31630  occllem  31655  shjshsi  31844  3oalem4  32017  pjfi  32056  dmadjss  32239  nlelshi  32412  nlelchi  32413  hmopidmchi  32503  shatomistici  32713  difxp1ss  32868  difxp2ss  32869  fcoinver  32949  opabssi  32958  mptctf  33061  ccatws1f1o  33271  gsumpart  33383  pmtrcnel2  33410  psgnfzto1stlem  33420  cycpmrn  33463  cyc3genpm  33472  unitprodclb  33702  lsmsnorb  33704  ply1degltel  33884  ply1degleel  33885  ply1degltlss  33886  evlextv  33932  vietalem  33969  constrsscn  34130  cnre2csqima  34301  raddcn  34319  zrhcntr  34369  rrhre  34411  esumsnf  34454  sxbrsiga  34680  omssubadd  34690  carsggect  34708  sitmcl  34741  oddpwdc  34744  eulerpartlem1  34757  eulerpartlemt  34761  eulerpartgbij  34762  eulerpartlemmf  34765  eulerpartlemgh  34768  sseqf  34782  ballotlemfmpn  34885  ballotth  34928  signswch  34948  ftc2re  34985  fdvposlt  34986  fdvposle  34988  bnj1146  35179  bnj1292  35203  bnj1293  35204  bnj1145  35381  bnj1177  35394  fineqvnttrclse  35537  tz9.1regs  35547  erdszelem2  35684  kur14lem3  35700  kur14lem6  35703  kur14lem7  35704  kur14lem9  35706  cvmlift2lem12  35806  mpstssv  36031  mstapst  36039  mppspstlem  36063  mppspst  36066  mthmsta  36070  mthmpps  36074  mclsppslem  36075  txpss3v  36368  pprodss4v  36374  relsset  36378  fixssdm  36396  fixssrn  36397  limitssson  36401  funpartss  36436  colinearex  36552  fneer  36884  neibastop1  36890  neibastop2lem  36891  filnetlem2  36910  filnetlem3  36911  ttcuniun  37041  ttcuni  37044  knoppcnlem10  37111  bj-tagss  37636  bj-imdirco  37854  bj-fvsnun2  37920  bj-ablssgrp  37940  bj-ablsscmn  37942  bj-vecssmod  37945  bj-fldssdrng  37952  icoreresf  38018  icoreunrn  38025  poimirlem29  38320  poimirlem30  38321  poimirlem31  38322  poimir  38324  broucube  38325  dvasin  38375  dvacos  38376  areacirc  38384  caures  38431  bnd2lem  38462  ismtyres  38479  flddivrng  38670  xrnss3v  39050  refrelsredund2  39386  toycom  39767  dihglblem2N  42088  lcdvbase  42387  mapdunirnN  42444  aks6d1c1p1rcl  42895  redvmptabs  43141  readvrec  43143  prjspreln0  43361  prjspvs  43362  prjspeclsp  43364  0prjspnrel  43379  dffltz  43386  eldiophb  43508  monotuz  43688  pwssplit4  43836  pwfi2f1o  43843  arearect  43962  cantnfresb  44071  omabs2  44079  fvnonrel  44343  rclexi  44361  rtrclex  44363  trclexi  44366  rtrclexi  44367  clcnvlem  44369  cnvrcl0  44371  cnvtrcl0  44372  dfrtrcl5  44375  dfrcl2  44420  comptiunov2i  44452  corclrcl  44453  trclrelexplem  44457  relexpaddss  44464  cotrcltrcl  44471  corcltrcl  44485  cotrclrcl  44488  frege131d  44510  0he  44528  grumnudlem  45015  uzmptshftfval  45076  binomcxplemdvbinom  45083  binomcxplemdvsum  45085  binomcxplemnotnn0  45086  modelaxreplem2  45708  rabexgf  45764  uzct  45803  disjf1o  45929  dmmptssf  45967  mptssid  45976  uzfissfz  46062  ssuzfz  46085  uzssre2  46141  uzublem  46164  uzssz2  46190  uzsscn2  46211  sumnnodd  46366  climconstmpt  46392  fnlimfvre  46408  fnlimabslt  46413  limsupubuzlem  46446  limsupubuz  46447  limsupequzmpt2  46452  limsupmnfuzlem  46460  limsupre3uzlem  46469  liminfequzmpt2  46525  ibliooicc  46705  stoweidlem44  46778  stoweidlem50  46784  stoweidlem51  46785  stoweidlem52  46786  stoweidlem57  46791  stoweidlem59  46793  fourierdlem16  46857  fourierdlem19  46860  fourierdlem21  46862  fourierdlem22  46863  fourierdlem42  46883  fourierdlem83  46923  fouriersw  46965  salexct  47068  salexct3  47076  salgencntex  47077  salgensscntex  47078  sge0less  47126  sge0fodjrnlem  47150  sge0isum  47161  ovnlerp  47296  ovn0lem  47299  hoidmv1lelem1  47325  hoidmv1lelem3  47327  hoidmvlelem1  47329  hoidmvlelem2  47330  hoidmvlelem3  47331  hoidmvlelem4  47332  ovnhoilem1  47335  ovnhoilem2  47336  opnvonmbllem2  47367  ovolval4lem1  47383  ovolval5lem3  47388  pimdecfgtioc  47449  pimincfltioc  47450  pimdecfgtioo  47451  pimincfltioo  47452  incsmflem  47475  decsmflem  47500  smflimlem2  47506  smflimlem3  47507  smflim  47511  smfrec  47523  smfmullem4  47528  smfdiv  47531  smfsuplem1  47545  smfsuplem3  47547  smfsupxr  47550  smfliminflem  47564  cfsetssfset  47813  fcoreslem2  47821  fcores  47824  gricrel  48704  clnbgrisubgrgrim  48717  isubgr3stgrlem6  48756  isubgr3stgrlem7  48757  isubgr3stgrlem8  48758  isubgr3stgr  48760  grlimgrtrilem2  48787  grlicrel  48791  oddibas  48958  2zlidl  49025  2zrngbas  49027  2zrng0  49029  fldcALTV  49117  fldhmsubcALTV  49118  dmtposss  49674  tposres3  49679  ipolub0  49790  imaidfu  49908