Theorem eqsstri 3977

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

This proof depends on syntax axioms:   = wceq 1570   ⊆ wss 3899

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2753  df-ss 3916

This theorem is used by:  eqsstrri  3978  3sstr4i  3982  ssrab3  4030  rabssab  4033  ifssun  4500  opabss  5169  brab2a  5744  relopabiALT  5801  dmopabss  5900  rnopabss  5937  resss  5992  relres  5996  rninOLD  6138  rnxpss  6164  cnvcnvss  6186  cnvcnvssOLD  6187  resdmss  6236  resssxp  6272  dfpo2  6299  predss  6312  fnres  6666  f0  6763  nfvres  6923  fvopab4ndm  7024  ffvresb  7126  mptexgf  7228  funiunfv  7252  isoini2  7347  ovssunirn  7456  dmoprabss  7524  mpondm0  7661  elmpocl  7662  exse2  7929  frxp  8138  tposssxp  8247  dftpos4  8262  smores  8360  smores2  8362  iordsmo  8365  swoer  8749  swoord1  8750  swoord2  8751  ecss  8769  ecopovsym  8840  ecopovtrn  8841  ecopover  8842  f1setex  8879  sbthlem7  9112  imafi  9307  elfiun  9422  marypha1lem  9425  marypha2lem1  9427  hartogslem1  9536  wdomima2g  9580  inf3lem1  9629  dmttrcl  9722  rnttrcl  9723  tc2  9741  frmin  9753  frrlem16  9762  frr1  9763  tz9.12lem1  9794  rankuni  9879  rankuniss  9883  rankmapu  9895  hta  9962  htaOLD  9963  r0weon  10091  infxpenlem  10092  ackbij1lem9  10305  ackbij1lem10  10306  ackbij1b  10316  sdom2en01  10380  fin23lem26  10403  fin56  10471  fin1a2lem9  10486  axdc3lem  10528  axdc3lem2  10529  axcclem  10535  imadomg  10613  iundom2g  10624  smobeth  10671  canth4  10732  gruina  10903  grur1a  10904  pinn  10963  niex  10966  ltsopi  10973  ltrelpi  10974  dmaddpi  10975  dmmulpi  10976  enqex  11007  ltrelnq  11011  nqerf  11015  nqerrel  11017  dmrecnq  11053  lterpq  11055  ltrelpr  11083  enrex  11152  ltrelsr  11153  dmaddsr  11170  dmmulsr  11171  ltrelre  11219  axaddf  11230  axmulf  11231  ltrelxr  11370  lerelxr  11372  nn0ssre  12610  nn0sscn  12611  nn0ssz  12716  uzsupss  13067  rpnnen1lem1  13106  rpnnen1lem3  13107  rpnnen1lem5  13109  fz1ssfz0  13757  uzsup  14003  fzfi  14115  swrd00  14792  01sqrexlem3  15411  cau3  15523  caubnd  15526  limsupgre  15648  rlimpm  15667  rlimclim  15713  isercolllem1  15832  isercolllem2  15833  isercoll  15835  caurcvg  15844  caucvg  15846  iseraltlem2  15850  iseraltlem3  15851  zsum  15884  fsumcvg3  15895  climfsum  15987  ackbijnn  15997  divcnvshft  16024  infcvgaux1i  16026  clim2prod  16057  ntrivcvg  16066  ntrivcvgfvn0  16068  ntrivcvgtail  16069  ntrivcvgmullem  16070  ntrivcvgmul  16071  zprod  16104  dvdszrcl  16427  4sqlem1  17126  4sqlem19  17141  ramub1lem2  17205  structcnvcnv  17331  strleun  17335  fvsetsid  17346  idressidex0  18860  smndex1sgrp  19107  gicer  19491  cntzsgrpcl  19548  symgbasfi  19593  mvdco  19659  symgsssg  19681  efglem  19930  efgtf  19936  efgtlen  19940  efginvrel2  19941  efginvrel1  19942  efgsfo  19953  efgredlemg  19956  efgredleme  19957  efgredlemd  19958  efgredlemc  19959  efgredlem  19961  efgred  19962  efgrelexlemb  19964  efgcpbllemb  19969  frgpinv  19978  frgpuplem  19986  frgpupf  19987  frgpup1  19989  frgpnabllem2  20088  gsumval3lem1  20119  gsumval3lem2  20120  gsumval3  20121  ricrel  20744  fldc  21041  fldhmsubc  21042  lbsextlem3  21438  pzriprnglem10  21796  znf1o  21857  zntoslem  21862  pjpm  22014  mhp0cl  22467  ply1bascl  22521  dmtopon  23241  ordtbas  23510  leordtval2  23530  lecldbas  23537  lmfval  23550  lmbrf  23578  cnconst2  23601  conncompcld  23752  hauspwdom  23820  txuni2  23884  xkouni  23918  xkoccn  23938  txkgen  23971  qtoptop2  24018  kqdisj  24051  hmphtop  24097  hmpher  24103  uzrest  24216  uzfbas  24217  lmflf  24324  tgpconncompeqg  24431  tgpconncomp  24432  ustn0  24540  xmeter  24752  isngp2  24916  xrtgioo  25126  iccntr  25141  xmetdcn  25158  metdcn  25160  metdscn2  25177  cnheiborlem  25275  reparphti  25318  lmmbrf  25583  iscau4  25600  iscauf  25601  caucfil  25604  lmclimf  25625  volf  25850  uniioombllem3  25906  uniioombllem4  25907  uniioombllem5  25908  volcn  25927  mbfimaopnlem  25976  mbflimsup  25987  i1f1  26011  itg2lcl  26048  itgioo  26136  itgsplitioo  26158  limcflflem  26200  limcflf  26201  limcresi  26205  lhop  26336  dvfsumlem1  26346  dvfsumlem2  26347  dvfsumlem3  26348  dvfsumlem4  26349  dvfsumrlimge0  26350  dvfsumrlim  26351  dvfsumrlim2  26352  dvfsum2  26354  vieta1lem1  26633  vieta1lem2  26634  psercnlem2  26751  psercnlem1  26752  psercn  26753  pserdvlem1  26754  pserdvlem2  26755  pserdv  26756  pserdv2  26757  logcnlem5  26974  dvlog  26979  dvlog2lem  26980  dvlog2  26981  dvcncxp1  27071  dvcnsqrt  27072  cxpcn3lem  27075  cxpcn3  27076  sqrtcn  27078  1cubr  27170  atansssdm  27261  jensen  27316  musum  27518  ppiub  27531  lgsquadlem1  27707  lgsquadlem2  27708  lgsquadlem3  27709  2sqlem7  27751  nosupbnd1lem1  28065  nosupbnd2  28073  noinfbnd1lem1  28080  cutsf  28178  leftssold  28257  rightssold  28258  mulsproplem12  28513  mulsproplem13  28514  mulsproplem14  28515  precsexlem8  28600  onssno  28640  nnssn0s  28707  dfnns2  28758  bdaypw2n0bndlem  28849  axtgcgrrflx  28924  axtgcgrid  28925  axtgsegcon  28926  axtg5seg  28927  axtgbtwnid  28928  axtgpasch  28929  axtgcont1  28930  tglng  29009  disjxwwlkn  30502  frgrwopreg2  30920  phnv  31416  htthlem  31519  hlimadd  31795  hlimcaui  31838  hhsscms  31880  occllem  31905  shjshsi  32094  3oalem4  32267  pjfi  32306  dmadjss  32489  nlelshi  32662  nlelchi  32663  hmopidmchi  32753  shatomistici  32963  difxp1ss  33118  difxp2ss  33119  fcoinver  33198  opabssi  33207  mptctf  33308  ccatws1f1o  33514  gsumpart  33624  pmtrcnel2  33651  psgnfzto1stlem  33661  cycpmrn  33704  cyc3genpm  33713  unitprodclb  33944  lsmsnorb  33946  ply1degltel  34126  ply1degleel  34127  ply1degltlss  34128  evlextv  34174  vietalem  34211  constrsscn  34372  cnre2csqima  34543  raddcn  34561  zrhcntr  34611  rrhre  34653  esumsnf  34696  sxbrsiga  34922  omssubadd  34932  carsggect  34950  sitmcl  34983  oddpwdc  34986  eulerpartlem1  34999  eulerpartlemt  35003  eulerpartgbij  35004  eulerpartlemmf  35007  eulerpartlemgh  35010  sseqf  35024  ballotlemfmpn  35127  ballotth  35170  signswch  35190  ftc2re  35227  fdvposlt  35228  fdvposle  35230  bnj1146  35421  bnj1292  35445  bnj1293  35446  bnj1145  35623  bnj1177  35636  fineqvnttrclse  35792  tz9.1regs  35802  erdszelem2  35957  kur14lem3  35973  kur14lem6  35976  kur14lem7  35977  kur14lem9  35979  cvmlift2lem12  36079  mpstssv  36304  mstapst  36312  mppspstlem  36336  mppspst  36339  mthmsta  36343  mthmpps  36347  mclsppslem  36348  txpss3v  36640  pprodss4v  36646  relsset  36650  fixssdm  36668  fixssrn  36669  limitssson  36673  funpartss  36708  colinearex  36825  fneer  37141  neibastop1  37147  neibastop2lem  37148  filnetlem2  37167  filnetlem3  37168  ttcuniun  37298  ttcuni  37301  knoppcnlem10  37368  bj-tagss  37893  bj-imdirco  38111  bj-fvsnun2  38177  bj-ablssgrp  38197  bj-ablsscmn  38199  bj-vecssmod  38202  bj-fldssdrng  38209  icoreresf  38275  icoreunrn  38282  poimirlem29  38567  poimirlem30  38568  poimirlem31  38569  poimir  38571  broucube  38572  dvasin  38622  dvacos  38623  areacirc  38631  caures  38694  bnd2lem  38725  ismtyres  38742  flddivrng  38933  xrnss3v  39313  refrelsredund2  39649  toycom  40030  dihglblem2N  42351  lcdvbase  42650  mapdunirnN  42707  aks6d1c1p1rcl  43158  redvmptabs  43411  readvrec  43413  prjspreln0  43637  prjspvs  43638  prjspeclsp  43640  frlmnzcoordcl2  43656  prjspnnorm  43661  0prjspnrel  43663  dffltz  43670  eldiophb  43767  monotuz  43947  pwssplit4  44090  pwfi2f1o  44097  arearect  44216  cantnfresb  44325  omabs2  44333  fvnonrel  44596  rclexi  44614  rtrclex  44616  trclexi  44619  rtrclexi  44620  clcnvlem  44622  cnvrcl0  44624  cnvtrcl0  44625  dfrtrcl5  44628  dfrcl2  44673  comptiunov2i  44705  corclrcl  44706  trclrelexplem  44710  relexpaddss  44717  cotrcltrcl  44724  corcltrcl  44738  cotrclrcl  44741  frege131d  44763  0he  44781  grumnudlem  45268  uzmptshftfval  45329  binomcxplemdvbinom  45336  binomcxplemdvsum  45338  binomcxplemnotnn0  45339  modelaxreplem2  45968  rabexgf  46040  uzct  46079  disjf1o  46205  dmmptssf  46243  mptssid  46252  uzfissfz  46337  ssuzfz  46360  uzssre2  46416  uzublem  46439  uzssz2  46465  uzsscn2  46486  sumnnodd  46641  climconstmpt  46667  fnlimfvre  46683  fnlimabslt  46688  limsupubuzlem  46721  limsupubuz  46722  limsupequzmpt2  46727  limsupmnfuzlem  46735  limsupre3uzlem  46744  liminfequzmpt2  46800  ibliooicc  46980  stoweidlem44  47053  stoweidlem50  47059  stoweidlem51  47060  stoweidlem52  47061  stoweidlem57  47066  stoweidlem59  47068  fourierdlem16  47132  fourierdlem19  47135  fourierdlem21  47137  fourierdlem22  47138  fourierdlem42  47158  fourierdlem83  47198  fouriersw  47240  salexct  47343  salexct3  47351  salgencntex  47352  salgensscntex  47353  sge0less  47401  sge0fodjrnlem  47425  sge0isum  47436  ovnlerp  47571  ovn0lem  47574  hoidmv1lelem1  47600  hoidmv1lelem3  47602  hoidmvlelem1  47604  hoidmvlelem2  47605  hoidmvlelem3  47606  hoidmvlelem4  47607  ovnhoilem1  47610  ovnhoilem2  47611  opnvonmbllem2  47642  ovolval4lem1  47658  ovolval5lem3  47663  pimdecfgtioc  47724  pimincfltioc  47725  pimdecfgtioo  47726  pimincfltioo  47727  incsmflem  47750  decsmflem  47775  smflimlem2  47781  smflimlem3  47782  smflim  47786  smfrec  47798  smfmullem4  47803  smfdiv  47806  smfsuplem1  47820  smfsuplem3  47822  smfsupxr  47825  smfliminflem  47839  cfsetssfset  48125  fcoreslem2  48133  fcores  48136  gricrel  49016  clnbgrisubgrgrim  49029  isubgr3stgrlem6  49068  isubgr3stgrlem7  49069  isubgr3stgrlem8  49070  isubgr3stgr  49072  grlimgrtrilem2  49099  grlicrel  49103  oddibas  49269  2zlidl  49336  2zrngbas  49338  2zrng0  49340  fldcALTV  49428  fldhmsubcALTV  49429  dmtposss  49983  tposres3  49988  ipolub0  50099  imaidfu  50217