Theorem eqsstri 3984

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

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

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 2156  ax-ext 2737

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

This theorem is used by:  eqsstrri  3985  3sstr4i  3989  ssrab3  4037  rabssab  4040  ifssun  4507  opabss  5177  brab2a  5756  relopabiALT  5812  dmopabss  5910  rnopabss  5947  resss  6002  relres  6006  rninOLD  6146  rnxpss  6172  cnvcnvss  6194  cnvcnvssOLD  6195  resdmss  6238  resssxp  6274  dfpo2  6301  predss  6314  fnres  6666  f0  6763  nfvres  6923  fvopab4ndm  7024  ffvresb  7125  mptexgf  7227  funiunfv  7251  isoini2  7346  ovssunirn  7455  dmoprabss  7523  mpondm0  7660  elmpocl  7661  exse2  7920  frxp  8128  tposssxp  8232  dftpos4  8247  smores  8345  smores2  8347  iordsmo  8350  swoer  8732  swoord1  8733  swoord2  8734  ecss  8752  ecopovsym  8823  ecopovtrn  8824  ecopover  8825  f1setex  8860  sbthlem7  9088  imafi  9282  elfiun  9397  marypha1lem  9400  marypha2lem1  9402  hartogslem1  9511  wdomima2g  9555  inf3lem1  9604  dmttrcl  9697  rnttrcl  9698  tc2  9716  frmin  9728  frrlem16  9737  frr1  9738  tz9.12lem1  9766  rankuni  9842  rankuniss  9845  rankmapu  9857  hta  9898  htaOLD  9899  r0weon  10012  infxpenlem  10013  ackbij1lem9  10226  ackbij1lem10  10227  ackbij1b  10237  sdom2en01  10301  fin23lem26  10324  fin56  10392  fin1a2lem9  10407  axdc3lem  10449  axdc3lem2  10450  axcclem  10456  imadomg  10534  iundom2g  10543  smobeth  10590  canth4  10651  gruina  10822  grur1a  10823  pinn  10882  niex  10885  ltsopi  10892  ltrelpi  10893  dmaddpi  10894  dmmulpi  10895  enqex  10926  ltrelnq  10930  nqerf  10934  nqerrel  10936  dmrecnq  10972  lterpq  10974  ltrelpr  11002  enrex  11071  ltrelsr  11072  dmaddsr  11089  dmmulsr  11090  ltrelre  11138  axaddf  11149  axmulf  11150  ltrelxr  11289  lerelxr  11291  nn0ssre  12527  nn0sscn  12528  nn0ssz  12633  uzsupss  12984  rpnnen1lem1  13022  rpnnen1lem3  13023  rpnnen1lem5  13025  fz1ssfz0  13672  uzsup  13918  fzfi  14030  swrd00  14706  01sqrexlem3  15323  cau3  15435  caubnd  15438  limsupgre  15560  rlimpm  15579  rlimclim  15625  isercolllem1  15744  isercolllem2  15745  isercoll  15747  caurcvg  15756  caucvg  15758  iseraltlem2  15762  iseraltlem3  15763  zsum  15796  fsumcvg3  15807  climfsum  15899  ackbijnn  15909  divcnvshft  15936  infcvgaux1i  15938  clim2prod  15969  ntrivcvg  15978  ntrivcvgfvn0  15980  ntrivcvgtail  15981  ntrivcvgmullem  15982  ntrivcvgmul  15983  zprod  16018  dvdszrcl  16341  4sqlem1  17034  4sqlem19  17049  ramub1lem2  17113  structcnvcnv  17239  strleun  17243  fvsetsid  17254  idressidex0  18767  smndex1sgrp  19011  gicer  19395  cntzsgrpcl  19452  symgbasfi  19497  mvdco  19563  symgsssg  19585  efglem  19834  efgtf  19840  efgtlen  19844  efginvrel2  19845  efginvrel1  19846  efgsfo  19857  efgredlemg  19860  efgredleme  19861  efgredlemd  19862  efgredlemc  19863  efgredlem  19865  efgred  19866  efgrelexlemb  19868  efgcpbllemb  19873  frgpinv  19882  frgpuplem  19890  frgpupf  19891  frgpup1  19893  frgpnabllem2  19992  gsumval3lem1  20023  gsumval3lem2  20024  gsumval3  20025  ricrel  20646  fldc  20941  fldhmsubc  20942  lbsextlem3  21338  pzriprnglem10  21694  znf1o  21755  zntoslem  21760  pjpm  21912  mhp0cl  22363  ply1bascl  22417  dmtopon  23134  ordtbas  23403  leordtval2  23423  lecldbas  23430  lmfval  23443  lmbrf  23471  cnconst2  23494  conncompcld  23645  hauspwdom  23713  txuni2  23777  xkouni  23811  xkoccn  23831  txkgen  23864  qtoptop2  23911  kqdisj  23944  hmphtop  23990  hmpher  23996  uzrest  24109  uzfbas  24110  lmflf  24217  tgpconncompeqg  24324  tgpconncomp  24325  ustn0  24433  xmeter  24645  isngp2  24809  xrtgioo  25019  iccntr  25034  xmetdcn  25051  metdcn  25053  metdscn2  25070  cnheiborlem  25168  reparphti  25211  lmmbrf  25476  iscau4  25493  iscauf  25494  caucfil  25497  lmclimf  25518  volf  25743  uniioombllem3  25799  uniioombllem4  25800  uniioombllem5  25801  volcn  25820  mbfimaopnlem  25869  mbflimsup  25880  i1f1  25904  itg2lcl  25941  itgioo  26030  itgsplitioo  26052  limcflflem  26094  limcflf  26095  limcresi  26099  lhop  26230  dvfsumlem1  26240  dvfsumlem2  26241  dvfsumlem3  26242  dvfsumlem4  26243  dvfsumrlimge0  26244  dvfsumrlim  26245  dvfsumrlim2  26246  dvfsum2  26248  vieta1lem1  26526  vieta1lem2  26527  psercnlem2  26642  psercnlem1  26643  psercn  26644  pserdvlem1  26645  pserdvlem2  26646  pserdv  26647  pserdv2  26648  logcnlem5  26866  dvlog  26871  dvlog2lem  26872  dvlog2  26873  dvcncxp1  26963  dvcnsqrt  26964  cxpcn3lem  26967  cxpcn3  26968  sqrtcn  26970  1cubr  27062  atansssdm  27153  jensen  27208  musum  27410  ppiub  27423  lgsquadlem1  27599  lgsquadlem2  27600  lgsquadlem3  27601  2sqlem7  27643  nosupbnd1lem1  27927  nosupbnd2  27935  noinfbnd1lem1  27942  cutsf  28040  leftssold  28119  rightssold  28120  mulsproplem12  28375  mulsproplem13  28376  mulsproplem14  28377  precsexlem8  28462  onssno  28502  nnssn0s  28569  dfnns2  28620  bdaypw2n0bndlem  28711  axtgcgrrflx  28786  axtgcgrid  28787  axtgsegcon  28788  axtg5seg  28789  axtgbtwnid  28790  axtgpasch  28791  axtgcont1  28792  tglng  28870  disjxwwlkn  30333  frgrwopreg2  30745  phnv  31241  htthlem  31344  hlimadd  31620  hlimcaui  31663  hhsscms  31705  occllem  31730  shjshsi  31919  3oalem4  32092  pjfi  32131  dmadjss  32314  nlelshi  32487  nlelchi  32488  hmopidmchi  32578  shatomistici  32788  difxp1ss  32943  difxp2ss  32944  fcoinver  33024  opabssi  33033  mptctf  33135  ccatws1f1o  33341  gsumpart  33451  pmtrcnel2  33478  psgnfzto1stlem  33488  cycpmrn  33531  cyc3genpm  33540  unitprodclb  33770  lsmsnorb  33772  ply1degltel  33952  ply1degleel  33953  ply1degltlss  33954  evlextv  34000  vietalem  34037  constrsscn  34198  cnre2csqima  34369  raddcn  34387  zrhcntr  34437  rrhre  34479  esumsnf  34522  sxbrsiga  34749  omssubadd  34759  carsggect  34777  sitmcl  34810  oddpwdc  34813  eulerpartlem1  34826  eulerpartlemt  34830  eulerpartgbij  34831  eulerpartlemmf  34834  eulerpartlemgh  34837  sseqf  34851  ballotlemfmpn  34954  ballotth  34997  signswch  35017  ftc2re  35054  fdvposlt  35055  fdvposle  35057  bnj1146  35248  bnj1292  35272  bnj1293  35273  bnj1145  35450  bnj1177  35463  fineqvnttrclse  35598  tz9.1regs  35608  erdszelem2  35725  kur14lem3  35741  kur14lem6  35744  kur14lem7  35745  kur14lem9  35747  cvmlift2lem12  35847  mpstssv  36072  mstapst  36080  mppspstlem  36104  mppspst  36107  mthmsta  36111  mthmpps  36115  mclsppslem  36116  txpss3v  36409  pprodss4v  36415  relsset  36419  fixssdm  36437  fixssrn  36438  limitssson  36442  funpartss  36477  colinearex  36593  fneer  36925  neibastop1  36931  neibastop2lem  36932  filnetlem2  36951  filnetlem3  36952  ttcuniun  37082  ttcuni  37085  knoppcnlem10  37152  bj-tagss  37677  bj-imdirco  37895  bj-fvsnun2  37961  bj-ablssgrp  37981  bj-ablsscmn  37983  bj-vecssmod  37986  bj-fldssdrng  37993  icoreresf  38059  icoreunrn  38066  poimirlem29  38361  poimirlem30  38362  poimirlem31  38363  poimir  38365  broucube  38366  dvasin  38416  dvacos  38417  areacirc  38425  caures  38473  bnd2lem  38504  ismtyres  38521  flddivrng  38712  xrnss3v  39092  refrelsredund2  39428  toycom  39809  dihglblem2N  42130  lcdvbase  42429  mapdunirnN  42486  aks6d1c1p1rcl  42937  redvmptabs  43198  readvrec  43200  prjspreln0  43418  prjspvs  43419  prjspeclsp  43421  0prjspnrel  43436  dffltz  43443  eldiophb  43565  monotuz  43745  pwssplit4  43893  pwfi2f1o  43900  arearect  44019  cantnfresb  44128  omabs2  44136  fvnonrel  44400  rclexi  44418  rtrclex  44420  trclexi  44423  rtrclexi  44424  clcnvlem  44426  cnvrcl0  44428  cnvtrcl0  44429  dfrtrcl5  44432  dfrcl2  44477  comptiunov2i  44509  corclrcl  44510  trclrelexplem  44514  relexpaddss  44521  cotrcltrcl  44528  corcltrcl  44542  cotrclrcl  44545  frege131d  44567  0he  44585  grumnudlem  45072  uzmptshftfval  45133  binomcxplemdvbinom  45140  binomcxplemdvsum  45142  binomcxplemnotnn0  45143  modelaxreplem2  45765  rabexgf  45821  uzct  45860  disjf1o  45986  dmmptssf  46024  mptssid  46033  uzfissfz  46119  ssuzfz  46142  uzssre2  46198  uzublem  46221  uzssz2  46247  uzsscn2  46268  sumnnodd  46423  climconstmpt  46449  fnlimfvre  46465  fnlimabslt  46470  limsupubuzlem  46503  limsupubuz  46504  limsupequzmpt2  46509  limsupmnfuzlem  46517  limsupre3uzlem  46526  liminfequzmpt2  46582  ibliooicc  46762  stoweidlem44  46835  stoweidlem50  46841  stoweidlem51  46842  stoweidlem52  46843  stoweidlem57  46848  stoweidlem59  46850  fourierdlem16  46914  fourierdlem19  46917  fourierdlem21  46919  fourierdlem22  46920  fourierdlem42  46940  fourierdlem83  46980  fouriersw  47022  salexct  47125  salexct3  47133  salgencntex  47134  salgensscntex  47135  sge0less  47183  sge0fodjrnlem  47207  sge0isum  47218  ovnlerp  47353  ovn0lem  47356  hoidmv1lelem1  47382  hoidmv1lelem3  47384  hoidmvlelem1  47386  hoidmvlelem2  47387  hoidmvlelem3  47388  hoidmvlelem4  47389  ovnhoilem1  47392  ovnhoilem2  47393  opnvonmbllem2  47424  ovolval4lem1  47440  ovolval5lem3  47445  pimdecfgtioc  47506  pimincfltioc  47507  pimdecfgtioo  47508  pimincfltioo  47509  incsmflem  47532  decsmflem  47557  smflimlem2  47563  smflimlem3  47564  smflim  47568  smfrec  47580  smfmullem4  47585  smfdiv  47588  smfsuplem1  47602  smfsuplem3  47604  smfsupxr  47607  smfliminflem  47621  cfsetssfset  47870  fcoreslem2  47878  fcores  47881  gricrel  48761  clnbgrisubgrgrim  48774  isubgr3stgrlem6  48813  isubgr3stgrlem7  48814  isubgr3stgrlem8  48815  isubgr3stgr  48817  grlimgrtrilem2  48844  grlicrel  48848  oddibas  49014  2zlidl  49081  2zrngbas  49083  2zrng0  49085  fldcALTV  49173  fldhmsubcALTV  49174  dmtposss  49730  tposres3  49735  ipolub0  49846  imaidfu  49964